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

Metamath Proof Explorer

Theorem brrpssg

Description: The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion brrpssg ( 𝐵 ∈ 𝑉 → ( 𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
2 relrpss ⊢ Rel [⊊]
3 2 brrelex1i ⊢ ( 𝐴 [⊊] 𝐵 → 𝐴 ∈ V )
4 1 3 anim12i ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 [⊊] 𝐵 ) → ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) )
5 1 adantr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊊ 𝐵 ) → 𝐵 ∈ V )
6 pssss ⊢ ( 𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵 )
7 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
8 6 1 7 syl2anr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊊ 𝐵 ) → 𝐴 ∈ V )
9 5 8 jca ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊊ 𝐵 ) → ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) )
10 psseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊊ 𝑦 ↔ 𝐴 ⊊ 𝑦 ) )
11 psseq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ⊊ 𝑦 ↔ 𝐴 ⊊ 𝐵 ) )
12 df-rpss ⊢ [⊊] = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊊ 𝑦 }
13 10 11 12 brabg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )
14 13 ancoms ⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )
15 4 9 14 pm5.21nd ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 [⊊] 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )