Metamath Proof Explorer


Theorem sbc2rexgOLD

Description: Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014) Obsolete as of 24-Aug-2018. Use csbov123 instead. (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sbc2rexgOLD
|- ( A e. V -> ( [. A / a ]. E. b e. B E. c e. C ph <-> E. b e. B E. c e. C [. A / a ]. ph ) )

Proof

Step Hyp Ref Expression
1 elex
 |-  ( A e. V -> A e. _V )
2 sbcrexgOLD
 |-  ( A e. _V -> ( [. A / a ]. E. b e. B E. c e. C ph <-> E. b e. B [. A / a ]. E. c e. C ph ) )
3 sbcrexgOLD
 |-  ( A e. _V -> ( [. A / a ]. E. c e. C ph <-> E. c e. C [. A / a ]. ph ) )
4 3 rexbidv
 |-  ( A e. _V -> ( E. b e. B [. A / a ]. E. c e. C ph <-> E. b e. B E. c e. C [. A / a ]. ph ) )
5 2 4 bitrd
 |-  ( A e. _V -> ( [. A / a ]. E. b e. B E. c e. C ph <-> E. b e. B E. c e. C [. A / a ]. ph ) )
6 1 5 syl
 |-  ( A e. V -> ( [. A / a ]. E. b e. B E. c e. C ph <-> E. b e. B E. c e. C [. A / a ]. ph ) )