Metamath Proof Explorer


Theorem elunirnALT

Description: Alternate proof of elunirn . It is shorter but requires ax-pow (through eluniima , funiunfv , ndmfv ). (Contributed by NM, 24-Sep-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion elunirnALT FunFAranFxdomFAFx

Proof

Step Hyp Ref Expression
1 imadmrn FdomF=ranF
2 1 unieqi FdomF=ranF
3 2 eleq2i AFdomFAranF
4 eluniima FunFAFdomFxdomFAFx
5 3 4 bitr3id FunFAranFxdomFAFx