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

Theorem cbvrexfw 3305
Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3361 with a disjoint variable condition, which does not require ax-13 2377. For a version not dependent on ax-11 2157 and ax-12, see cbvrexvw 3238. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2141, ax-13 2377. (Revised by GG, 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 1857 . . . 4 𝑦 ¬ 𝜑
5 cbvrexfw.4 . . . . 5 𝑥𝜓
65nfn 1857 . . . 4 𝑥 ¬ 𝜓
7 cbvrexfw.5 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜓))
87notbid 318 . . . 4 (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
91, 2, 4, 6, 8cbvralfw 3304 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ∀𝑦𝐴 ¬ 𝜓)
10 ralnex 3072 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
11 ralnex 3072 . . 3 (∀𝑦𝐴 ¬ 𝜓 ↔ ¬ ∃𝑦𝐴 𝜓)
129, 10, 113bitr3i 301 . 2 (¬ ∃𝑥𝐴 𝜑 ↔ ¬ ∃𝑦𝐴 𝜓)
1312con4bii 321 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wnf 1783  wnfc 2890  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071
This theorem is referenced by:  cbvrexw  3307  reusv2lem4  5401  reusv2  5403  nnwof  12956  cbviunf  32568  ac6sf2  32634  dfimafnf  32646  aciunf1lem  32672  bnj1400  34849  phpreu  37611  poimirlem26  37653  indexa  37740  evth2f  45020  fvelrnbf  45023  evthf  45032  eliin2f  45109  stoweidlem34  46049  ovnlerp  46577
  Copyright terms: Public domain W3C validator