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

Theorem cbvrexfw 3422
Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3424 with a disjoint variable condition, which does not require ax-13 2392. (Contributed by FL, 27-Apr-2008.) (Revised by Gino Giotto, 10-Jan-2024.)
Hypotheses
Ref Expression
cbvrexfw.1 𝑥𝐴
cbvrexfw.2 𝑦𝐴
cbvrexfw.3 𝑦𝜑
cbvrexfw.4 𝑥𝜓
cbvrexfw.5 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrexfw (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem cbvrexfw
StepHypRef Expression
1 cbvrexfw.1 . . . 4 𝑥𝐴
2 cbvrexfw.2 . . . 4 𝑦𝐴
3 cbvrexfw.3 . . . . 5 𝑦𝜑
43nfn 1858 . . . 4 𝑦 ¬ 𝜑
5 cbvrexfw.4 . . . . 5 𝑥𝜓
65nfn 1858 . . . 4 𝑥 ¬ 𝜓
7 cbvrexfw.5 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
87notbid 321 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
91, 2, 4, 6, 8cbvralfw 3420 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑦𝐴 ¬ 𝜓)
109notbii 323 . 2 (¬ ∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦𝐴 ¬ 𝜓)
11 dfrex2 3233 . 2 (∃𝑥𝐴 𝜑 ↔ ¬ ∀𝑥𝐴 ¬ 𝜑)
12 dfrex2 3233 . 2 (∃𝑦𝐴 𝜓 ↔ ¬ ∀𝑦𝐴 ¬ 𝜓)
1310, 11, 123bitr4i 306 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wnf 1785  wnfc 2962  wral 3133  wrex 3134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-11 2162  ax-12 2179
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-clel 2896  df-nfc 2964  df-ral 3138  df-rex 3139
This theorem is referenced by:  cbvrexw  3426  reusv2lem4  5290  reusv2  5292  nnwof  12313  cbviunf  30325  ac6sf2  30389  dfimafnf  30400  aciunf1lem  30426  bnj1400  32192  phpreu  35013  poimirlem26  35055  indexa  35143  evth2f  41592  fvelrnbf  41595  evthf  41604  eliin2f  41690  stoweidlem34  42629  ovnlerp  43154
  Copyright terms: Public domain W3C validator