Theorem rababg

Description: Condition when restricted class is equal to unrestricted class. (Contributed by RP, 13-Aug-2020)

	Ref	Expression
Assertion	rababg	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝐴 ) ↔ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		ancrb	⊢ ( ( 𝜑 → 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
2	1	albii	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝐴 ) ↔ ∀ 𝑥 ( 𝜑 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
3		nfv	⊢ Ⅎ 𝑦 ( 𝜑 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
4		nfsab1	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 }
5		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝜑 }
6	5	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 }
7	4 6	nfim	⊢ Ⅎ 𝑥 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } )
8		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
9		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
10	8 9	bitr3id	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
11		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
12		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) )
13	11 12	bitr3id	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) )
14	10 13	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) ) )
15	3 7 14	cbvalv1	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) )
16		eqss	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ 𝜑 } ↔ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜑 } ∧ { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) )
17		rabssab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜑 }
18	17	biantrur	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜑 } ∧ { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) )
19		dfss2	⊢ ( { 𝑥 ∣ 𝜑 } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) )
20	16 18 19	3bitr2ri	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) ↔ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ 𝜑 } )
21	2 15 20	3bitri	⊢ ( ∀ 𝑥 ( 𝜑 → 𝑥 ∈ 𝐴 ) ↔ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ 𝜑 } )