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 ( ∃* 𝑥𝐴 ( 𝑥𝐴𝜑 ) ↔ ∃* 𝑥𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 anabs5 ( ( 𝑥𝐴 ∧ ( 𝑥𝐴𝜑 ) ) ↔ ( 𝑥𝐴𝜑 ) )
2 1 mobii ( ∃* 𝑥 ( 𝑥𝐴 ∧ ( 𝑥𝐴𝜑 ) ) ↔ ∃* 𝑥 ( 𝑥𝐴𝜑 ) )
3 df-rmo ( ∃* 𝑥𝐴 ( 𝑥𝐴𝜑 ) ↔ ∃* 𝑥 ( 𝑥𝐴 ∧ ( 𝑥𝐴𝜑 ) ) )
4 df-rmo ( ∃* 𝑥𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥𝐴𝜑 ) )
5 2 3 4 3bitr4i ( ∃* 𝑥𝐴 ( 𝑥𝐴𝜑 ) ↔ ∃* 𝑥𝐴 𝜑 )