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

Theorem cbvralf 3313
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 2009 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvralf.1 . . . . . 6 𝑥𝐴
32nfcri 2901 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2287 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfim 1995 . . . 4 𝑥(𝑧𝐴 → [𝑧 / 𝑥]𝜑)
6 eleq1w 2827 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2278 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7imbi12d 335 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 → [𝑧 / 𝑥]𝜑)))
91, 5, 8cbval 2376 . . 3 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑧(𝑧𝐴 → [𝑧 / 𝑥]𝜑))
10 cbvralf.2 . . . . . 6 𝑦𝐴
1110nfcri 2901 . . . . 5 𝑦 𝑧𝐴
12 cbvralf.3 . . . . . 6 𝑦𝜑
1312nfsb 2534 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfim 1995 . . . 4 𝑦(𝑧𝐴 → [𝑧 / 𝑥]𝜑)
15 nfv 2009 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1w 2827 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2467 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvralf.4 . . . . . . 7 𝑥𝜓
19 cbvralf.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbie 2499 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 278 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21imbi12d 335 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 → [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbval 2376 . . 3 (∀𝑧(𝑧𝐴 → [𝑧 / 𝑥]𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
249, 23bitri 266 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
25 df-ral 3060 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
26 df-ral 3060 . 2 (∀𝑦𝐴 𝜓 ↔ ∀𝑦(𝑦𝐴𝜓))
2724, 25, 263bitr4i 294 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wal 1650  wnf 1878  [wsb 2062  wcel 2155  wnfc 2894  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clel 2761  df-nfc 2896  df-ral 3060
This theorem is referenced by:  cbvrexf  3314  cbvral  3315  reusv2lem4  5038  reusv2  5040  ffnfvf  6581  nnwof  11958  nnindf  30017  scottexf  34400  scott0f  34401  evth2f  39829  evthf  39841  supxrleubrnmptf  40320  stoweidlem14  40871  stoweidlem28  40885  stoweidlem59  40916
  Copyright terms: Public domain W3C validator