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

Theorem cbvrexf 3141
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 1767 . . . 4 𝑦 ¬ 𝜑
5 cbvralf.4 . . . . 5 𝑥𝜓
65nfn 1767 . . . 4 𝑥 ¬ 𝜓
7 cbvralf.5 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
87notbid 306 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
91, 2, 4, 6, 8cbvralf 3140 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑦𝐴 ¬ 𝜓)
109notbii 308 . 2 (¬ ∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦𝐴 ¬ 𝜓)
11 dfrex2 2978 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
12 dfrex2 2978 . 2 (∃𝑦𝐴 𝜓 ↔ ¬ ∀𝑦𝐴 ¬ 𝜓)
1310, 11, 123bitr4i 290 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wnf 1698  wnfc 2737  wral 2895  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901
This theorem is referenced by:  cbvrex  3143  reusv2lem4  4793  reusv2  4795  nnwof  11586  cbviunf  28561  ac6sf2  28616  dfimafnf  28623  aciunf1lem  28650  bnj1400  29966  phpreu  32359  poimirlem26  32401  indexa  32494  evth2f  37993  fvelrnbf  37996  evthf  38005  eliin2f  38112  stoweidlem34  38724  ovnlerp  39249
  Copyright terms: Public domain W3C validator