Theorem cbvrexf 3141

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 1767	. . . 4 ⊢ Ⅎ𝑦 ¬ 𝜑
5		cbvralf.4	. . . . 5 ⊢ Ⅎ𝑥𝜓
6	5	nfn 1767	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜓
7		cbvralf.5	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
8	7	notbid 306	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
9	1, 2, 4, 6, 8	cbvralf 3140	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
10	9	notbii 308	. 2 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
11		dfrex2 2978	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
12		dfrex2 2978	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ¬ ∀𝑦 ∈ 𝐴 ¬ 𝜓)
13	10, 11, 12	3bitr4i 290	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 194  Ⅎwnf 1698  Ⅎwnfc 2737  ∀wral 2895  ∃wrex 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901

This theorem is referenced by:  cbvrex  3143  reusv2lem4  4793  reusv2  4795  nnwof  11586  cbviunf  28561  ac6sf2  28616  dfimafnf  28623  aciunf1lem  28650  bnj1400  29966  phpreu  32359  poimirlem26  32401  indexa  32494  evth2f  37993  fvelrnbf  37996  evthf  38005  eliin2f  38112  stoweidlem34  38724  ovnlerp  39249