Theorem ralrmo3

Description: Pull a restricted universal quantifier into the body (for E* ). (Contributed by Peter Mazsa, 9-May-2019)

	Ref	Expression
Assertion	ralrmo3	|- ( A. y e. B E* x e. A ph <-> A. y E* x e. A ( y e. B /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-ral	|- ( A. y e. B E* x e. A ph <-> A. y ( y e. B -> E* x e. A ph ) )
2		nfv	|- F/ x y e. B
3	2	rmoanim	|- ( E* x e. A ( y e. B /\ ph ) <-> ( y e. B -> E* x e. A ph ) )
4	3	albii	|- ( A. y E* x e. A ( y e. B /\ ph ) <-> A. y ( y e. B -> E* x e. A ph ) )
5	1 4	bitr4i	|- ( A. y e. B E* x e. A ph <-> A. y E* x e. A ( y e. B /\ ph ) )