Theorem cbvrexf 3301

Description: Rule used to change bound variables, using implicit substitution. (Contributed by FL, 27-Apr-2008.) (Revised by Mario Carneiro, 9-Oct-2016.)

Hypotheses

Ref	Expression
cbvralf.1	⊢ Ⅎ𝑥𝐴
cbvralf.2	⊢ Ⅎ𝑦𝐴
cbvralf.3	⊢ Ⅎ𝑦𝜑
cbvralf.4	⊢ Ⅎ𝑥𝜓
cbvralf.5	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrexf	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Proof of Theorem cbvrexf

Step	Hyp	Ref	Expression
1		cbvralf.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2		cbvralf.2	. . . 4 ⊢ Ⅎ𝑦𝐴
3		cbvralf.3	. . . . 5 ⊢ Ⅎ𝑦𝜑
4	3	nfn 1929	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
5		cbvralf.4	. . . . 5 ⊢ Ⅎ𝑥𝜓
6	5	nfn 1929	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
7		cbvralf.5	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
8	7	notbid 307	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
9	1, 2, 4, 6, 8	cbvralf 3300	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
10	9	notbii 309	. 2 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
11		dfrex2 3130	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
12		dfrex2 3130	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
13	10, 11, 12	3bitr4i 292	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196  Ⅎwnf 1853  Ⅎwnfc 2885  ∀wral 3046  ∃wrex 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clel 2752  df-nfc 2887  df-ral 3051  df-rex 3052

This theorem is referenced by:  cbvrex  3303  reusv2lem4  5017  reusv2  5019  nnwof  11943  cbviunf  29675  ac6sf2  29734  dfimafnf  29741  aciunf1lem  29767  bnj1400  31209  phpreu  33702  poimirlem26  33744  indexa  33837  evth2f  39669  fvelrnbf  39672  evthf  39681  eliin2f  39782  stoweidlem34  40750  ovnlerp  41278