# Metamath Proof Explorer

## Theorem sbcie2s

Description: A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Hypotheses sbcie2s.a ${⊢}{A}={E}\left({W}\right)$
sbcie2s.b ${⊢}{B}={F}\left({W}\right)$
sbcie2s.1 ${⊢}\left({a}={A}\wedge {b}={B}\right)\to \left({\phi }↔{\psi }\right)$
Assertion sbcie2s

### Proof

Step Hyp Ref Expression
1 sbcie2s.a ${⊢}{A}={E}\left({W}\right)$
2 sbcie2s.b ${⊢}{B}={F}\left({W}\right)$
3 sbcie2s.1 ${⊢}\left({a}={A}\wedge {b}={B}\right)\to \left({\phi }↔{\psi }\right)$
4 fvex ${⊢}{E}\left({w}\right)\in \mathrm{V}$
5 fvex ${⊢}{F}\left({w}\right)\in \mathrm{V}$
6 simprl ${⊢}\left({w}={W}\wedge \left({a}={E}\left({w}\right)\wedge {b}={F}\left({w}\right)\right)\right)\to {a}={E}\left({w}\right)$
7 fveq2 ${⊢}{w}={W}\to {E}\left({w}\right)={E}\left({W}\right)$
8 7 1 eqtr4di ${⊢}{w}={W}\to {E}\left({w}\right)={A}$
9 8 adantr ${⊢}\left({w}={W}\wedge \left({a}={E}\left({w}\right)\wedge {b}={F}\left({w}\right)\right)\right)\to {E}\left({w}\right)={A}$
10 6 9 eqtrd ${⊢}\left({w}={W}\wedge \left({a}={E}\left({w}\right)\wedge {b}={F}\left({w}\right)\right)\right)\to {a}={A}$
11 simprr ${⊢}\left({w}={W}\wedge \left({a}={E}\left({w}\right)\wedge {b}={F}\left({w}\right)\right)\right)\to {b}={F}\left({w}\right)$
12 fveq2 ${⊢}{w}={W}\to {F}\left({w}\right)={F}\left({W}\right)$
13 12 2 eqtr4di ${⊢}{w}={W}\to {F}\left({w}\right)={B}$
14 13 adantr ${⊢}\left({w}={W}\wedge \left({a}={E}\left({w}\right)\wedge {b}={F}\left({w}\right)\right)\right)\to {F}\left({w}\right)={B}$
15 11 14 eqtrd ${⊢}\left({w}={W}\wedge \left({a}={E}\left({w}\right)\wedge {b}={F}\left({w}\right)\right)\right)\to {b}={B}$
16 10 15 3 syl2anc ${⊢}\left({w}={W}\wedge \left({a}={E}\left({w}\right)\wedge {b}={F}\left({w}\right)\right)\right)\to \left({\phi }↔{\psi }\right)$
17 16 bicomd ${⊢}\left({w}={W}\wedge \left({a}={E}\left({w}\right)\wedge {b}={F}\left({w}\right)\right)\right)\to \left({\psi }↔{\phi }\right)$
18 17 ex ${⊢}{w}={W}\to \left(\left({a}={E}\left({w}\right)\wedge {b}={F}\left({w}\right)\right)\to \left({\psi }↔{\phi }\right)\right)$
19 4 5 18 sbc2iedv