This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝜓 } ⊆ { 𝑥 ∈ 𝐵 ∣ 𝜓 } )