Theorem cbvrexfw 3273

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3327 with a disjoint variable condition, which does not require ax-13 2372. For a version not dependent on ax-11 2160 and ax-12, see cbvrexvw 3211. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2144, ax-13 2372. (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 1858	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
5		cbvrexfw.4	. . . . 5 ⊢ Ⅎ𝑥𝜓
6	5	nfn 1858	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
7		cbvrexfw.5	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
8	7	notbid 318	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
9	1, 2, 4, 6, 8	cbvralfw 3272	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
10		ralnex 3058	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
11		ralnex 3058	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓)
12	9, 10, 11	3bitr3i 301	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓)
13	12	con4bii 321	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  Ⅎwnf 1784  Ⅎwnfc 2879  ∀wral 3047  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-11 2160  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057

This theorem is referenced by:  cbvrexw  3275  reusv2lem4  5337  reusv2  5339  nnwof  12812  cbviunf  32535  ac6sf2  32605  dfimafnf  32618  aciunf1lem  32644  bnj1400  34847  phpreu  37652  poimirlem26  37694  indexa  37781  evth2f  45060  fvelrnbf  45063  evthf  45072  eliin2f  45149  stoweidlem34  46080  ovnlerp  46608