Theorem rexxfr2d 5348

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 5347	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ¬ 𝜓 ↔ ∀𝑦 ∈ 𝐶 ¬ 𝜒))
6	5	notbid 318	. 2 ⊢ (𝜑 → (¬ ∀𝑥 ∈ 𝐵 ¬ 𝜓 ↔ ¬ ∀𝑦 ∈ 𝐶 ¬ 𝜒))
7		dfrex2 3065	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ¬ ∀𝑥 ∈ 𝐵 ¬ 𝜓)
8		dfrex2 3065	. 2 ⊢ (∃𝑦 ∈ 𝐶 𝜒 ↔ ¬ ∀𝑦 ∈ 𝐶 ¬ 𝜒)
9	6, 7, 8	3bitr4g 314	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐶 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by:  rexrn  7033  reximaOLD  7187  cnpresti  23263  cnprest  23264  1stcrest  23428  subislly  23456  txrest  23606  trfil2  23862  met1stc  24496  metucn  24546  xrlimcnp  26945  esumlub  34220  esumfsup  34230  rexxfr3d  35836  ptrest  37954  djhcvat42  41875