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