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

Theorem cbvrexfw 3302
Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3357 with a disjoint variable condition, which does not require ax-13 2371. For a version not dependent on ax-11 2154 and ax-12, see cbvrexvw 3235. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2137, ax-13 2371. (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 1860 . . . 4 𝑦 ¬ 𝜑
5 cbvrexfw.4 . . . . 5 𝑥𝜓
65nfn 1860 . . . 4 𝑥 ¬ 𝜓
7 cbvrexfw.5 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
87notbid 317 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
91, 2, 4, 6, 8cbvralfw 3301 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑦𝐴 ¬ 𝜓)
10 ralnex 3072 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
11 ralnex 3072 . . 3 (∀𝑦𝐴 ¬ 𝜓 ↔ ¬ ∃𝑦𝐴 𝜓)
129, 10, 113bitr3i 300 . 2 (¬ ∃𝑥𝐴 𝜑 ↔ ¬ ∃𝑦𝐴 𝜓)
1312con4bii 320 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wnf 1785  wnfc 2883  wral 3061  wrex 3070
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-11 2154  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071
This theorem is referenced by:  cbvrexw  3304  reusv2lem4  5399  reusv2  5401  nnwof  12897  cbviunf  31782  ac6sf2  31844  dfimafnf  31855  aciunf1lem  31882  bnj1400  33841  phpreu  36467  poimirlem26  36509  indexa  36596  evth2f  43689  fvelrnbf  43692  evthf  43701  eliin2f  43783  stoweidlem34  44740  ovnlerp  45268
  Copyright terms: Public domain W3C validator