Theorem cbvrexfw 3306

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  Ⅎwnf 1813  Ⅎwnfc 2910  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090

This theorem is referenced by:  cbvrexw  3308  reusv2lem4  5372  reusv2  5374  nnwof  12933  cbviunf  32900  ac6sf2  32967  dfimafnf  32981  aciunf1lem  33007  bnj1400  35223  phpreu  38255  poimirlem26  38297  indexa  38384  evth2f  45735  fvelrnbf  45738  evthf  45747  eliin2f  45822  stoweidlem34  46748  ovnlerp  47276