This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbcabel

Description: Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005)

Ref Expression
Hypothesis sbcabel.1 
|- F/_ x B
Assertion sbcabel 
|- ( A e. V -> ( [. A / x ]. { y | ph } e. B <-> { y | [. A / x ]. ph } e. B ) )

Proof

Step Hyp Ref Expression
1 sbcabel.1 
 |-  F/_ x B
2 elex 
 |-  ( A e. V -> A e. _V )
3 sbcex2 
 |-  ( [. A / x ]. E. w ( w = { y | ph } /\ w e. B ) <-> E. w [. A / x ]. ( w = { y | ph } /\ w e. B ) )
4 sbcan 
 |-  ( [. A / x ]. ( w = { y | ph } /\ w e. B ) <-> ( [. A / x ]. w = { y | ph } /\ [. A / x ]. w e. B ) )
5 sbcal 
 |-  ( [. A / x ]. A. y ( y e. w <-> ph ) <-> A. y [. A / x ]. ( y e. w <-> ph ) )
6 sbcbig 
 |-  ( A e. _V -> ( [. A / x ]. ( y e. w <-> ph ) <-> ( [. A / x ]. y e. w <-> [. A / x ]. ph ) ) )
7 sbcg 
 |-  ( A e. _V -> ( [. A / x ]. y e. w <-> y e. w ) )
8 7 bibi1d 
 |-  ( A e. _V -> ( ( [. A / x ]. y e. w <-> [. A / x ]. ph ) <-> ( y e. w <-> [. A / x ]. ph ) ) )
9 6 8 bitrd 
 |-  ( A e. _V -> ( [. A / x ]. ( y e. w <-> ph ) <-> ( y e. w <-> [. A / x ]. ph ) ) )
10 9 albidv 
 |-  ( A e. _V -> ( A. y [. A / x ]. ( y e. w <-> ph ) <-> A. y ( y e. w <-> [. A / x ]. ph ) ) )
11 5 10 bitrid 
 |-  ( A e. _V -> ( [. A / x ]. A. y ( y e. w <-> ph ) <-> A. y ( y e. w <-> [. A / x ]. ph ) ) )
12 eqabb 
 |-  ( w = { y | ph } <-> A. y ( y e. w <-> ph ) )
13 12 sbcbii 
 |-  ( [. A / x ]. w = { y | ph } <-> [. A / x ]. A. y ( y e. w <-> ph ) )
14 eqabb 
 |-  ( w = { y | [. A / x ]. ph } <-> A. y ( y e. w <-> [. A / x ]. ph ) )
15 11 13 14 3bitr4g 
 |-  ( A e. _V -> ( [. A / x ]. w = { y | ph } <-> w = { y | [. A / x ]. ph } ) )
16 1 nfcri 
 |-  F/ x w e. B
17 16 sbcgf 
 |-  ( A e. _V -> ( [. A / x ]. w e. B <-> w e. B ) )
18 15 17 anbi12d 
 |-  ( A e. _V -> ( ( [. A / x ]. w = { y | ph } /\ [. A / x ]. w e. B ) <-> ( w = { y | [. A / x ]. ph } /\ w e. B ) ) )
19 4 18 bitrid 
 |-  ( A e. _V -> ( [. A / x ]. ( w = { y | ph } /\ w e. B ) <-> ( w = { y | [. A / x ]. ph } /\ w e. B ) ) )
20 19 exbidv 
 |-  ( A e. _V -> ( E. w [. A / x ]. ( w = { y | ph } /\ w e. B ) <-> E. w ( w = { y | [. A / x ]. ph } /\ w e. B ) ) )
21 3 20 bitrid 
 |-  ( A e. _V -> ( [. A / x ]. E. w ( w = { y | ph } /\ w e. B ) <-> E. w ( w = { y | [. A / x ]. ph } /\ w e. B ) ) )
22 dfclel 
 |-  ( { y | ph } e. B <-> E. w ( w = { y | ph } /\ w e. B ) )
23 22 sbcbii 
 |-  ( [. A / x ]. { y | ph } e. B <-> [. A / x ]. E. w ( w = { y | ph } /\ w e. B ) )
24 dfclel 
 |-  ( { y | [. A / x ]. ph } e. B <-> E. w ( w = { y | [. A / x ]. ph } /\ w e. B ) )
25 21 23 24 3bitr4g 
 |-  ( A e. _V -> ( [. A / x ]. { y | ph } e. B <-> { y | [. A / x ]. ph } e. B ) )
26 2 25 syl 
 |-  ( A e. V -> ( [. A / x ]. { y | ph } e. B <-> { y | [. A / x ]. ph } e. B ) )