# Metamath Proof Explorer

## Theorem sbcop1

Description: The proper substitution of an ordered pair for a setvar variable corresponds to a proper substitution of its first component. (Contributed by AV, 8-Apr-2023)

Ref Expression
Hypothesis sbcop.z ${⊢}{z}=⟨{x},{y}⟩\to \left({\phi }↔{\psi }\right)$
Assertion sbcop1

### Proof

Step Hyp Ref Expression
1 sbcop.z ${⊢}{z}=⟨{x},{y}⟩\to \left({\phi }↔{\psi }\right)$
2 sbc5
3 opeq1 ${⊢}{a}={x}\to ⟨{a},{y}⟩=⟨{x},{y}⟩$
4 3 equcoms ${⊢}{x}={a}\to ⟨{a},{y}⟩=⟨{x},{y}⟩$
5 4 eqeq2d ${⊢}{x}={a}\to \left({z}=⟨{a},{y}⟩↔{z}=⟨{x},{y}⟩\right)$
6 1 biimprd ${⊢}{z}=⟨{x},{y}⟩\to \left({\psi }\to {\phi }\right)$
7 5 6 syl6bi ${⊢}{x}={a}\to \left({z}=⟨{a},{y}⟩\to \left({\psi }\to {\phi }\right)\right)$
8 7 com23 ${⊢}{x}={a}\to \left({\psi }\to \left({z}=⟨{a},{y}⟩\to {\phi }\right)\right)$
9 8 imp ${⊢}\left({x}={a}\wedge {\psi }\right)\to \left({z}=⟨{a},{y}⟩\to {\phi }\right)$
10 9 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={a}\wedge {\psi }\right)\to \left({z}=⟨{a},{y}⟩\to {\phi }\right)$
11 2 10 sylbi
12 11 alrimiv
13 opex ${⊢}⟨{a},{y}⟩\in \mathrm{V}$
14 13 sbc6
15 12 14 sylibr
16 sbc5
17 1 biimpd ${⊢}{z}=⟨{x},{y}⟩\to \left({\phi }\to {\psi }\right)$
18 5 17 syl6bi ${⊢}{x}={a}\to \left({z}=⟨{a},{y}⟩\to \left({\phi }\to {\psi }\right)\right)$
19 18 com3l ${⊢}{z}=⟨{a},{y}⟩\to \left({\phi }\to \left({x}={a}\to {\psi }\right)\right)$
20 19 imp ${⊢}\left({z}=⟨{a},{y}⟩\wedge {\phi }\right)\to \left({x}={a}\to {\psi }\right)$
21 20 alrimiv ${⊢}\left({z}=⟨{a},{y}⟩\wedge {\phi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={a}\to {\psi }\right)$
22 vex ${⊢}{a}\in \mathrm{V}$
23 22 sbc6
24 21 23 sylibr
25 24 exlimiv
26 16 25 sylbi
27 15 26 impbii