Metamath Proof Explorer


Theorem rabbiiaOLD

Description: Obsolete version of rabbiia as of 12-Jan-2025. (Contributed by NM, 22-May-1999) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis rabbiia.1 x A φ ψ
Assertion rabbiiaOLD x A | φ = x A | ψ

Proof

Step Hyp Ref Expression
1 rabbiia.1 x A φ ψ
2 1 pm5.32i x A φ x A ψ
3 2 abbii x | x A φ = x | x A ψ
4 df-rab x A | φ = x | x A φ
5 df-rab x A | ψ = x | x A ψ
6 3 4 5 3eqtr4i x A | φ = x A | ψ