# Metamath Proof Explorer

## Theorem sprsymrelf1lem

Description: Lemma for sprsymrelf1 . (Contributed by AV, 22-Nov-2021)

Ref Expression
Assertion sprsymrelf1lem ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\to \left(\left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\to {a}\subseteq {b}\right)$

### Proof

Step Hyp Ref Expression
1 prssspr ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {p}\in {a}\right)\to \exists {i}\in {V}\phantom{\rule{.4em}{0ex}}\exists {j}\in {V}\phantom{\rule{.4em}{0ex}}{p}=\left\{{i},{j}\right\}$
2 1 ad4ant14 ${⊢}\left(\left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\wedge {p}\in {a}\right)\to \exists {i}\in {V}\phantom{\rule{.4em}{0ex}}\exists {j}\in {V}\phantom{\rule{.4em}{0ex}}{p}=\left\{{i},{j}\right\}$
3 simpr ${⊢}\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\to {p}=\left\{{i},{j}\right\}$
4 3 adantr ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\to {p}=\left\{{i},{j}\right\}$
5 4 eleq1d ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\to \left({p}\in {a}↔\left\{{i},{j}\right\}\in {a}\right)$
6 simpr ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left\{{i},{j}\right\}\in {a}\right)\to \left\{{i},{j}\right\}\in {a}$
7 eqeq1 ${⊢}{c}=\left\{{i},{j}\right\}\to \left({c}=\left\{{i},{j}\right\}↔\left\{{i},{j}\right\}=\left\{{i},{j}\right\}\right)$
8 7 adantl ${⊢}\left(\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left\{{i},{j}\right\}\in {a}\right)\wedge {c}=\left\{{i},{j}\right\}\right)\to \left({c}=\left\{{i},{j}\right\}↔\left\{{i},{j}\right\}=\left\{{i},{j}\right\}\right)$
9 eqidd ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left\{{i},{j}\right\}\in {a}\right)\to \left\{{i},{j}\right\}=\left\{{i},{j}\right\}$
10 6 8 9 rspcedvd ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left\{{i},{j}\right\}\in {a}\right)\to \exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}$
11 10 adantlr ${⊢}\left(\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\wedge \left\{{i},{j}\right\}\in {a}\right)\to \exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}$
12 preq12 ${⊢}\left({x}={i}\wedge {y}={j}\right)\to \left\{{x},{y}\right\}=\left\{{i},{j}\right\}$
13 12 eqeq2d ${⊢}\left({x}={i}\wedge {y}={j}\right)\to \left({c}=\left\{{x},{y}\right\}↔{c}=\left\{{i},{j}\right\}\right)$
14 13 rexbidv ${⊢}\left({x}={i}\wedge {y}={j}\right)\to \left(\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}↔\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}\right)$
15 14 opelopabga ${⊢}\left({i}\in {V}\wedge {j}\in {V}\right)\to \left(⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}↔\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}\right)$
16 15 bicomd ${⊢}\left({i}\in {V}\wedge {j}\in {V}\right)\to \left(\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}↔⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)$
17 16 ad3antrrr ${⊢}\left(\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\wedge \left\{{i},{j}\right\}\in {a}\right)\to \left(\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}↔⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)$
18 11 17 mpbid ${⊢}\left(\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\wedge \left\{{i},{j}\right\}\in {a}\right)\to ⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}$
19 18 ex ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\to \left(\left\{{i},{j}\right\}\in {a}\to ⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)$
20 5 19 sylbid ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\to \left({p}\in {a}\to ⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)$
21 eleq2 ${⊢}\left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\to \left(⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}↔⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)$
22 21 ad2antll ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\to \left(⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}↔⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)$
23 13 rexbidv ${⊢}\left({x}={i}\wedge {y}={j}\right)\to \left(\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}↔\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}\right)$
24 23 opelopabga ${⊢}\left({i}\in \mathrm{V}\wedge {j}\in \mathrm{V}\right)\to \left(⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}↔\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}\right)$
25 24 el2v ${⊢}⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}↔\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}$
26 eqtr3 ${⊢}\left({p}=\left\{{i},{j}\right\}\wedge {c}=\left\{{i},{j}\right\}\right)\to {p}={c}$
27 26 equcomd ${⊢}\left({p}=\left\{{i},{j}\right\}\wedge {c}=\left\{{i},{j}\right\}\right)\to {c}={p}$
28 27 eleq1d ${⊢}\left({p}=\left\{{i},{j}\right\}\wedge {c}=\left\{{i},{j}\right\}\right)\to \left({c}\in {b}↔{p}\in {b}\right)$
29 28 biimpd ${⊢}\left({p}=\left\{{i},{j}\right\}\wedge {c}=\left\{{i},{j}\right\}\right)\to \left({c}\in {b}\to {p}\in {b}\right)$
30 29 ex ${⊢}{p}=\left\{{i},{j}\right\}\to \left({c}=\left\{{i},{j}\right\}\to \left({c}\in {b}\to {p}\in {b}\right)\right)$
31 30 com13 ${⊢}{c}\in {b}\to \left({c}=\left\{{i},{j}\right\}\to \left({p}=\left\{{i},{j}\right\}\to {p}\in {b}\right)\right)$
32 31 imp ${⊢}\left({c}\in {b}\wedge {c}=\left\{{i},{j}\right\}\right)\to \left({p}=\left\{{i},{j}\right\}\to {p}\in {b}\right)$
33 32 rexlimiva ${⊢}\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}\to \left({p}=\left\{{i},{j}\right\}\to {p}\in {b}\right)$
34 33 com12 ${⊢}{p}=\left\{{i},{j}\right\}\to \left(\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}\to {p}\in {b}\right)$
35 34 adantl ${⊢}\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\to \left(\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}\to {p}\in {b}\right)$
36 35 adantr ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\to \left(\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{i},{j}\right\}\to {p}\in {b}\right)$
37 25 36 syl5bi ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\to \left(⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\to {p}\in {b}\right)$
38 22 37 sylbid ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\to \left(⟨{i},{j}⟩\in \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\to {p}\in {b}\right)$
39 20 38 syld ${⊢}\left(\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\wedge \left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\right)\to \left({p}\in {a}\to {p}\in {b}\right)$
40 39 expimpd ${⊢}\left(\left({i}\in {V}\wedge {j}\in {V}\right)\wedge {p}=\left\{{i},{j}\right\}\right)\to \left(\left(\left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\wedge {p}\in {a}\right)\to {p}\in {b}\right)$
41 40 rexlimdva2 ${⊢}{i}\in {V}\to \left(\exists {j}\in {V}\phantom{\rule{.4em}{0ex}}{p}=\left\{{i},{j}\right\}\to \left(\left(\left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\wedge {p}\in {a}\right)\to {p}\in {b}\right)\right)$
42 41 rexlimiv ${⊢}\exists {i}\in {V}\phantom{\rule{.4em}{0ex}}\exists {j}\in {V}\phantom{\rule{.4em}{0ex}}{p}=\left\{{i},{j}\right\}\to \left(\left(\left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\wedge {p}\in {a}\right)\to {p}\in {b}\right)$
43 2 42 mpcom ${⊢}\left(\left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\wedge {p}\in {a}\right)\to {p}\in {b}$
44 43 ex ${⊢}\left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\to \left({p}\in {a}\to {p}\in {b}\right)$
45 44 ssrdv ${⊢}\left(\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\wedge \left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\right)\to {a}\subseteq {b}$
46 45 ex ${⊢}\left({a}\subseteq \mathrm{Pairs}\left({V}\right)\wedge {b}\subseteq \mathrm{Pairs}\left({V}\right)\right)\to \left(\left\{⟨{x},{y}⟩|\exists {c}\in {a}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}=\left\{⟨{x},{y}⟩|\exists {c}\in {b}\phantom{\rule{.4em}{0ex}}{c}=\left\{{x},{y}\right\}\right\}\to {a}\subseteq {b}\right)$