Theorem cbvrexfw 3360

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf 3362 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by FL, 27-Apr-2008.) (Revised by Gino Giotto, 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 1861	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
5		cbvrexfw.4	. . . . 5 ⊢ Ⅎ𝑥𝜓
6	5	nfn 1861	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
7		cbvrexfw.5	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
8	7	notbid 317	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
9	1, 2, 4, 6, 8	cbvralfw 3358	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
10	9	notbii 319	. 2 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
11		dfrex2 3166	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
12		dfrex2 3166	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
13	10, 11, 12	3bitr4i 302	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  Ⅎwnf 1787  Ⅎwnfc 2886  ∀wral 3063  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069

This theorem is referenced by:  cbvrexw  3364  reusv2lem4  5319  reusv2  5321  nnwof  12583  cbviunf  30796  ac6sf2  30861  dfimafnf  30872  aciunf1lem  30901  bnj1400  32715  phpreu  35688  poimirlem26  35730  indexa  35818  evth2f  42447  fvelrnbf  42450  evthf  42459  eliin2f  42543  stoweidlem34  43465  ovnlerp  43990