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 ( 𝐵𝑉 → ( 𝐴 [] 𝐵𝐴𝐵 ) )