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

Theorem cbvrexf 3158
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 1781 . . . 4 𝑦 ¬ 𝜑
5 cbvralf.4 . . . . 5 𝑥𝜓
65nfn 1781 . . . 4 𝑥 ¬ 𝜓
7 cbvralf.5 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
87notbid 308 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
91, 2, 4, 6, 8cbvralf 3157 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑦𝐴 ¬ 𝜓)
109notbii 310 . 2 (¬ ∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦𝐴 ¬ 𝜓)
11 dfrex2 2992 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
12 dfrex2 2992 . 2 (∃𝑦𝐴 𝜓 ↔ ¬ ∀𝑦𝐴 ¬ 𝜓)
1310, 11, 123bitr4i 292 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wnf 1705  wnfc 2748  wral 2908  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914
This theorem is referenced by:  cbvrex  3160  reusv2lem4  4842  reusv2  4844  nnwof  11714  cbviunf  29259  ac6sf2  29313  dfimafnf  29320  aciunf1lem  29345  bnj1400  30667  phpreu  33064  poimirlem26  33106  indexa  33199  evth2f  38696  fvelrnbf  38699  evthf  38708  eliin2f  38809  stoweidlem34  39588  ovnlerp  40113
  Copyright terms: Public domain W3C validator