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

Theorem cbvralf 3160
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 1841 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvralf.1 . . . . . 6 𝑥𝐴
32nfcri 2756 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2435 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfim 1823 . . . 4 𝑥(𝑧𝐴 → [𝑧 / 𝑥]𝜑)
6 eleq1 2687 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2109 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7imbi12d 334 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 → [𝑧 / 𝑥]𝜑)))
91, 5, 8cbval 2269 . . 3 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑧(𝑧𝐴 → [𝑧 / 𝑥]𝜑))
10 cbvralf.2 . . . . . 6 𝑦𝐴
1110nfcri 2756 . . . . 5 𝑦 𝑧𝐴
12 cbvralf.3 . . . . . 6 𝑦𝜑
1312nfsb 2438 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfim 1823 . . . 4 𝑦(𝑧𝐴 → [𝑧 / 𝑥]𝜑)
15 nfv 1841 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1 2687 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2374 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvralf.4 . . . . . . 7 𝑥𝜓
19 cbvralf.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbie 2406 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 276 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21imbi12d 334 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 → [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbval 2269 . . 3 (∀𝑧(𝑧𝐴 → [𝑧 / 𝑥]𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
249, 23bitri 264 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
25 df-ral 2914 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
26 df-ral 2914 . 2 (∀𝑦𝐴 𝜓 ↔ ∀𝑦(𝑦𝐴𝜓))
2724, 25, 263bitr4i 292 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1479  wnf 1706  [wsb 1878  wcel 1988  wnfc 2749  wral 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914
This theorem is referenced by:  cbvrexf  3161  cbvral  3162  reusv2lem4  4863  reusv2  4865  ffnfvf  6375  nnwof  11739  nnindf  29539  scottexf  33947  scott0f  33948  evth2f  38994  evthf  39006  supxrleubrnmptf  39493  stoweidlem14  39994  stoweidlem28  40008  stoweidlem59  40039
  Copyright terms: Public domain W3C validator