Theorem rabxfr 2959

Description: Abstraction class membership after substituting an expression A (containing y) for x in the class expression φ.

Hypotheses

Ref	Expression
rabxfr.1	⊢ (z ∈ B → ∀y z ∈ B)
rabxfr.2	⊢ (z ∈ C → ∀y z ∈ C)
rabxfr.3	⊢ (y ∈ D → A ∈ D)
rabxfr.4	⊢ (x = A → (φ ↔ ψ))
rabxfr.5	⊢ (y = B → A = C)

Assertion

Ref	Expression
rabxfr	⊢ (B ∈ D → (C ∈ {x ∈ D∣φ} ↔ B ∈ {y ∈ D∣ψ}))

Distinct variable groups:   x,A   z,B   z,C   x,y,z,D   φ,y,z   ψ,x,z

Proof of Theorem rabxfr

Step	Hyp	Ref	Expression
1		rabxfr.3	. . . . . . . 8 ⊢ (y ∈ D → A ∈ D)
2		ibibr 602	. . . . . . . 8 ⊢ ((y ∈ D → A ∈ D) ↔ (y ∈ D → (A ∈ D ↔ y ∈ D)))
3	1, 2	mpbi 196	. . . . . . 7 ⊢ (y ∈ D → (A ∈ D ↔ y ∈ D))
4	3	anbi1d 628	. . . . . 6 ⊢ (y ∈ D → ((A ∈ D ⋀ ψ) ↔ (y ∈ D ⋀ ψ)))
5		rabxfr.4	. . . . . . 7 ⊢ (x = A → (φ ↔ ψ))
6	5	elrab 1952	. . . . . 6 ⊢ (A ∈ {x ∈ D∣φ} ↔ (A ∈ D ⋀ ψ))
7		rabid 1816	. . . . . 6 ⊢ (y ∈ {y ∈ D∣ψ} ↔ (y ∈ D ⋀ ψ))
8	4, 6, 7	3bitr4g 566	. . . . 5 ⊢ (y ∈ D → (A ∈ {x ∈ D∣φ} ↔ y ∈ {y ∈ D∣ψ}))
9	8	rabbii 1852	. . . 4 ⊢ {y ∈ D∣A ∈ {x ∈ D∣φ}} = {y ∈ D∣y ∈ {y ∈ D∣ψ}}
10	9	eleq2i 1585	. . 3 ⊢ (B ∈ {y ∈ D∣A ∈ {x ∈ D∣φ}} ↔ B ∈ {y ∈ D∣y ∈ {y ∈ D∣ψ}})
11		rabxfr.1	. . . 4 ⊢ (z ∈ B → ∀y z ∈ B)
12		ax-17 1012	. . . 4 ⊢ (z ∈ D → ∀y z ∈ D)
13		rabxfr.2	. . . . 5 ⊢ (z ∈ C → ∀y z ∈ C)
14		ax-17 1012	. . . . 5 ⊢ (z ∈ {x ∈ D∣φ} → ∀y z ∈ {x ∈ D∣φ})
15	13, 14	hbel 1613	. . . 4 ⊢ (C ∈ {x ∈ D∣φ} → ∀y C ∈ {x ∈ D∣φ})
16		rabxfr.5	. . . . 5 ⊢ (y = B → A = C)
17	16	eleq1d 1587	. . . 4 ⊢ (y = B → (A ∈ {x ∈ D∣φ} ↔ C ∈ {x ∈ D∣φ}))
18	11, 12, 15, 17	elrabf 1951	. . 3 ⊢ (B ∈ {y ∈ D∣A ∈ {x ∈ D∣φ}} ↔ (B ∈ D ⋀ C ∈ {x ∈ D∣φ}))
19		hbrab1 1819	. . . . 5 ⊢ (z ∈ {y ∈ D∣ψ} → ∀y z ∈ {y ∈ D∣ψ})
20	11, 19	hbel 1613	. . . 4 ⊢ (B ∈ {y ∈ D∣ψ} → ∀y B ∈ {y ∈ D∣ψ})
21		eleq1 1581	. . . 4 ⊢ (y = B → (y ∈ {y ∈ D∣ψ} ↔ B ∈ {y ∈ D∣ψ}))
22	11, 12, 20, 21	elrabf 1951	. . 3 ⊢ (B ∈ {y ∈ D∣y ∈ {y ∈ D∣ψ}} ↔ (B ∈ D ⋀ B ∈ {y ∈ D∣ψ}))
23	10, 18, 22	3bitr3i 188	. 2 ⊢ ((B ∈ D ⋀ C ∈ {x ∈ D∣φ}) ↔ (B ∈ D ⋀ B ∈ {y ∈ D∣ψ}))
24		pm5.32 655	. 2 ⊢ ((B ∈ D → (C ∈ {x ∈ D∣φ} ↔ B ∈ {y ∈ D∣ψ})) ↔ ((B ∈ D ⋀ C ∈ {x ∈ D∣φ}) ↔ (B ∈ D ⋀ B ∈ {y ∈ D∣ψ})))
25	23, 24	mpbir 197	1 ⊢ (B ∈ D → (C ∈ {x ∈ D∣φ} ↔ B ∈ {y ∈ D∣ψ}))

Syntax hints:   → wi 3   ↔ wb 153   ⋀ wa 230  ∀wal 995   = wceq 997   ∈ wcel 999  {crab 1695

This theorem is referenced by:  reuunixfr 2963  dfuzi 6287

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-rab 1699  df-v 1859

Copyright terms: Public domain