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