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

Theorem cbvralf 3195
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 1883 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvralf.1 . . . . . 6 𝑥𝐴
32nfcri 2787 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2465 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfim 1865 . . . 4 𝑥(𝑧𝐴 → [𝑧 / 𝑥]𝜑)
6 eleq1 2718 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2149 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7imbi12d 333 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 → [𝑧 / 𝑥]𝜑)))
91, 5, 8cbval 2307 . . 3 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑧(𝑧𝐴 → [𝑧 / 𝑥]𝜑))
10 cbvralf.2 . . . . . 6 𝑦𝐴
1110nfcri 2787 . . . . 5 𝑦 𝑧𝐴
12 cbvralf.3 . . . . . 6 𝑦𝜑
1312nfsb 2468 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfim 1865 . . . 4 𝑦(𝑧𝐴 → [𝑧 / 𝑥]𝜑)
15 nfv 1883 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1 2718 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2404 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvralf.4 . . . . . . 7 𝑥𝜓
19 cbvralf.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbie 2436 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 276 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21imbi12d 333 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 → [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbval 2307 . . 3 (∀𝑧(𝑧𝐴 → [𝑧 / 𝑥]𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
249, 23bitri 264 . 2 (∀𝑥(𝑥𝐴𝜑) ↔ ∀𝑦(𝑦𝐴𝜓))
25 df-ral 2946 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
26 df-ral 2946 . 2 (∀𝑦𝐴 𝜓 ↔ ∀𝑦(𝑦𝐴𝜓))
2724, 25, 263bitr4i 292 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521  wnf 1748  [wsb 1937  wcel 2030  wnfc 2780  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946
This theorem is referenced by:  cbvrexf  3196  cbvral  3197  reusv2lem4  4902  reusv2  4904  ffnfvf  6429  nnwof  11792  nnindf  29693  scottexf  34106  scott0f  34107  evth2f  39488  evthf  39500  supxrleubrnmptf  39993  stoweidlem14  40549  stoweidlem28  40563  stoweidlem59  40594
  Copyright terms: Public domain W3C validator