Theorem ralxfr2d 5352

Description: Transfer universal quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by Mario Carneiro, 20-Aug-2014.)

Hypotheses

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

Assertion

Ref	Expression
ralxfr2d	⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒))

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

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

Proof of Theorem ralxfr2d

Step	Hyp	Ref	Expression
1		ralxfr2d.1	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝑉)
2		elisset 2815	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
3	1, 2	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ∃𝑥 𝑥 = 𝐴)
4		ralxfr2d.2	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐶 𝑥 = 𝐴))
5	4	biimprd 248	. . . . . . 7 ⊢ (𝜑 → (∃𝑦 ∈ 𝐶 𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
6		r19.23v 3160	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐶 (𝑥 = 𝐴 → 𝑥 ∈ 𝐵) ↔ (∃𝑦 ∈ 𝐶 𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
7	5, 6	sylibr 234	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ 𝐶 (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
8	7	r19.21bi 3225	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
9		eleq1 2821	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
10	8, 9	mpbidi 241	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (𝑥 = 𝐴 → 𝐴 ∈ 𝐵))
11	10	exlimdv 1934	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → (∃𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵))
12	3, 11	mpd 15	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝐴 ∈ 𝐵)
13	4	biimpa 476	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐶 𝑥 = 𝐴)
14		ralxfr2d.3	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
15	12, 13, 14	ralxfrd 5350	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐶 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058

This theorem is referenced by:  rexxfr2d  5353  ralrn  7030  ralima  7180  ralimaOLD  7183  cnrest2  23221  cnprest2  23225  connsuba  23355  subislly  23416  trfbas2  23778  trfil2  23822  flimrest  23918  fclsrest  23959  tsmssubm  24078  metucn  24506  ist0cld  33918  extoimad  44321