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

Theorem cbvrexf 3301
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.)
Hypotheses
Ref Expression
cbvralf.1 𝑥𝐴
cbvralf.2 𝑦𝐴
cbvralf.3 𝑦𝜑
cbvralf.4 𝑥𝜓
cbvralf.5 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrexf (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)

Proof of Theorem cbvrexf
StepHypRef Expression
1 cbvralf.1 . . . 4 𝑥𝐴
2 cbvralf.2 . . . 4 𝑦𝐴
3 cbvralf.3 . . . . 5 𝑦𝜑
43nfn 1929 . . . 4 𝑦 ¬ 𝜑
5 cbvralf.4 . . . . 5 𝑥𝜓
65nfn 1929 . . . 4 𝑥 ¬ 𝜓
7 cbvralf.5 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
87notbid 307 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
91, 2, 4, 6, 8cbvralf 3300 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑦𝐴 ¬ 𝜓)
109notbii 309 . 2 (¬ ∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦𝐴 ¬ 𝜓)
11 dfrex2 3130 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
12 dfrex2 3130 . 2 (∃𝑦𝐴 𝜓 ↔ ¬ ∀𝑦𝐴 ¬ 𝜓)
1310, 11, 123bitr4i 292 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196  Ⅎwnf 1853  Ⅎwnfc 2885  ∀wral 3046  ∃wrex 3047 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clel 2752  df-nfc 2887  df-ral 3051  df-rex 3052 This theorem is referenced by:  cbvrex  3303  reusv2lem4  5017  reusv2  5019  nnwof  11943  cbviunf  29675  ac6sf2  29734  dfimafnf  29741  aciunf1lem  29767  bnj1400  31209  phpreu  33702  poimirlem26  33744  indexa  33837  evth2f  39669  fvelrnbf  39672  evthf  39681  eliin2f  39782  stoweidlem34  40750  ovnlerp  41278
 Copyright terms: Public domain W3C validator