Metamath Proof Explorer

Theorem sbc2rex

Description: Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by NM, 24-Aug-2018)

Ref Expression
Assertion sbc2rex 
|- ( [. 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 sbcrex 
 |-  ( [. A / a ]. E. b e. B E. c e. C ph <-> E. b e. B [. A / a ]. E. c e. C ph )
2 sbcrex 
 |-  ( [. A / a ]. E. c e. C ph <-> E. c e. C [. A / a ]. ph )
3 2 rexbii 
 |-  ( E. b e. B [. A / a ]. E. c e. C ph <-> E. b e. B E. c e. C [. A / a ]. ph )
4 1 3 bitri 
 |-  ( [. A / a ]. E. b e. B E. c e. C ph <-> E. b e. B E. c e. C [. A / a ]. ph )