Metamath Proof Explorer


Theorem rmoanidOLD

Description: Obsolete version of rmoanid as of 12-Jan-2025. (Contributed by Peter Mazsa, 24-May-2018) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 anabs5
 |-  ( ( x e. A /\ ( x e. A /\ ph ) ) <-> ( x e. A /\ ph ) )
2 1 mobii
 |-  ( E* x ( x e. A /\ ( x e. A /\ ph ) ) <-> E* x ( x e. A /\ ph ) )
3 df-rmo
 |-  ( E* x e. A ( x e. A /\ ph ) <-> E* x ( x e. A /\ ( x e. A /\ ph ) ) )
4 df-rmo
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
5 2 3 4 3bitr4i
 |-  ( E* x e. A ( x e. A /\ ph ) <-> E* x e. A ph )