Metamath Proof Explorer

Theorem r19.26m

Description: Version of 19.26 and r19.26 with restricted quantifiers ranging over different classes. (Contributed by NM, 22-Feb-2004)

Ref Expression
Assertion r19.26m 
|- ( A. x ( ( x e. A -> ph ) /\ ( x e. B -> ps ) ) <-> ( A. x e. A ph /\ A. x e. B ps ) )

Proof

Step Hyp Ref Expression
1 19.26 
 |-  ( A. x ( ( x e. A -> ph ) /\ ( x e. B -> ps ) ) <-> ( A. x ( x e. A -> ph ) /\ A. x ( x e. B -> ps ) ) )
2 df-ral 
 |-  ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
3 df-ral 
 |-  ( A. x e. B ps <-> A. x ( x e. B -> ps ) )
4 2 3 anbi12i 
 |-  ( ( A. x e. A ph /\ A. x e. B ps ) <-> ( A. x ( x e. A -> ph ) /\ A. x ( x e. B -> ps ) ) )
5 1 4 bitr4i 
 |-  ( A. x ( ( x e. A -> ph ) /\ ( x e. B -> ps ) ) <-> ( A. x e. A ph /\ A. x e. B ps ) )