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  12900  cbviunf  31825  ac6sf2  31887  dfimafnf  31898  aciunf1lem  31925  bnj1400  33915  phpreu  36558  poimirlem26  36600  indexa  36687  evth2f  43781  fvelrnbf  43784  evthf  43793  eliin2f  43875  stoweidlem34  44829  ovnlerp  45357
  Copyright terms: Public domain W3C validator