Theorem cbvrexfw 3277

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3332 with a disjoint variable condition, which does not require ax-13 2370. For a version not dependent on ax-11 2158 and ax-12, see cbvrexvw 3214. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2142, ax-13 2370. (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

Step	Hyp	Ref	Expression
1		cbvrexfw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2		cbvrexfw.2	. . . 4 ⊢ Ⅎ𝑦𝐴
3		cbvrexfw.3	. . . . 5 ⊢ Ⅎ𝑦𝜑
4	3	nfn 1857	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
5		cbvrexfw.4	. . . . 5 ⊢ Ⅎ𝑥𝜓
6	5	nfn 1857	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
7		cbvrexfw.5	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
8	7	notbid 318	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
9	1, 2, 4, 6, 8	cbvralfw 3276	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
10		ralnex 3055	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
11		ralnex 3055	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓)
12	9, 10, 11	3bitr3i 301	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓)
13	12	con4bii 321	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  Ⅎwnf 1783  Ⅎwnfc 2876  ∀wral 3044  ∃wrex 3053

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 2008  ax-8 2111  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054

This theorem is referenced by:  cbvrexw  3279  reusv2lem4  5351  reusv2  5353  nnwof  12849  cbviunf  32457  ac6sf2  32521  dfimafnf  32533  aciunf1lem  32559  bnj1400  34798  phpreu  37571  poimirlem26  37613  indexa  37700  evth2f  44982  fvelrnbf  44985  evthf  44994  eliin2f  45071  stoweidlem34  46005  ovnlerp  46533