Theorem rexxfr2d 5417

Description: Transfer existential quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)

Hypotheses

Ref	Expression
ralxfr2d.1	⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉)
ralxfr2d.2	⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴))
ralxfr2d.3	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rexxfr2d	⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝑥,𝐶   𝜒,𝑥   𝜑,𝑥,𝑦   𝜓,𝑦

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑦)   𝐴(𝑦)   𝐶(𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem rexxfr2d

Step	Hyp	Ref	Expression
1		ralxfr2d.1	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉)
2		ralxfr2d.2	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴))
3		ralxfr2d.3	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
4	3	notbid 318	. . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (¬ 𝜓 ↔ ¬ 𝜒))
5	1, 2, 4	ralxfr2d 5416	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ¬ 𝜓 ↔ ∀𝑦 ∈ 𝐶 ¬ 𝜒))
6	5	notbid 318	. 2 ⊢ (𝜑 → (¬ ∀𝑥 ∈ 𝐵 ¬ 𝜓 ↔ ¬ ∀𝑦 ∈ 𝐶 ¬ 𝜒))
7		dfrex2 3071	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ¬ ∀𝑥 ∈ 𝐵 ¬ 𝜓)
8		dfrex2 3071	. 2 ⊢ (∃𝑦 ∈ 𝐶 𝜒 ↔ ¬ ∀𝑦 ∈ 𝐶 ¬ 𝜒)
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069

This theorem is referenced by:  rexrn  7107  reximaOLD  7259  cnpresti  23312  cnprest  23313  1stcrest  23477  subislly  23505  txrest  23655  trfil2  23911  met1stc  24550  metucn  24600  xrlimcnp  27026  esumlub  34041  esumfsup  34051  rexxfr3d  35623  ptrest  37606  djhcvat42  41398