Theorem rabss3d

Description: Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017)

	Ref	Expression
Hypothesis	rabss3d.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) → 𝑥 ∈ 𝐵 )
Assertion	rabss3d	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐵 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		rabss3d.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) → 𝑥 ∈ 𝐵 )
2		nfv	⊢ Ⅎ 𝑥 𝜑
3		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝜓 }
4		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐵 ∣ 𝜓 }
5		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) → 𝜓 )
6	1 5	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
7	6	ex	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
8		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) )
9		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜓 } ↔ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
10	7 8 9	3imtr4g	⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝜓 } → 𝑥 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜓 } ) )
11	2 3 4 10	ssrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐵 ∣ 𝜓 } )