MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvralf Structured version   Visualization version   GIF version

Theorem cbvralf 3314
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.)
Hypotheses
Ref Expression
cbvralf.1 𝑥𝐴
cbvralf.2 𝑦𝐴
cbvralf.3 𝑦𝜑
cbvralf.4 𝑥𝜓
cbvralf.5 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvralf (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)

Proof of Theorem cbvralf
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfv 1995 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvralf.1 . . . . . 6 𝑥𝐴
32nfcri 2907 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2274 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfim 1977 . . . 4 𝑥(𝑧𝐴 → [𝑧 / 𝑥]𝜑)
6 eleq1w 2833 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2267 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7imbi12d 333 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 → [𝑧 / 𝑥]𝜑)))
91, 5, 8cbval 2432 . . 3 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑧(𝑧𝐴 → [𝑧 / 𝑥]𝜑))
10 cbvralf.2 . . . . . 6 𝑦𝐴
1110nfcri 2907 . . . . 5 𝑦 𝑧𝐴
12 cbvralf.3 . . . . . 6 𝑦𝜑
1312nfsb 2590 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfim 1977 . . . 4 𝑦(𝑧𝐴 → [𝑧 / 𝑥]𝜑)
15 nfv 1995 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1w 2833 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2523 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvralf.4 . . . . . . 7 𝑥𝜓
19 cbvralf.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbie 2555 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 276 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21imbi12d 333 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 → [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbval 2432 . . 3 (∀𝑧(𝑧𝐴 → [𝑧 / 𝑥]𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
249, 23bitri 264 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
25 df-ral 3066 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
26 df-ral 3066 . 2 (∀𝑦𝐴 𝜓 ↔ ∀𝑦(𝑦𝐴𝜓))
2724, 25, 263bitr4i 292 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1629  wnf 1856  [wsb 2049  wcel 2145  wnfc 2900  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clel 2767  df-nfc 2902  df-ral 3066
This theorem is referenced by:  cbvrexf  3315  cbvral  3316  reusv2lem4  5001  reusv2  5003  ffnfvf  6531  nnwof  11957  nnindf  29905  scottexf  34308  scott0f  34309  evth2f  39696  evthf  39708  supxrleubrnmptf  40196  stoweidlem14  40748  stoweidlem28  40762  stoweidlem59  40793
  Copyright terms: Public domain W3C validator