Theorem cbvrexfw 3275

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3329 with a disjoint variable condition, which does not require ax-13 2374. For a version not dependent on ax-11 2162 and ax-12, see cbvrexvw 3213. (Contributed by FL, 27-Apr-2008.) Avoid ax-10 2146, ax-13 2374. (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 3274	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
10		ralnex 3060	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
11		ralnex 3060	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓)
12	9, 10, 11	3bitr3i 301	. 2 ⊢ (¬ ∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∃𝑦 ∈ 𝐴 𝜓)
13	12	con4bii 321	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  Ⅎwnf 1784  Ⅎwnfc 2881  ∀wral 3049  ∃wrex 3058

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 2115  ax-11 2162  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059

This theorem is referenced by:  cbvrexw  3277  reusv2lem4  5344  reusv2  5346  nnwof  12825  cbviunf  32579  ac6sf2  32649  dfimafnf  32663  aciunf1lem  32689  bnj1400  34940  phpreu  37744  poimirlem26  37786  indexa  37873  evth2f  45202  fvelrnbf  45205  evthf  45214  eliin2f  45290  stoweidlem34  46220  ovnlerp  46748