Theorem alrimdv 1688

Description: Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.)

Hypothesis

Ref	Expression
alrimdv.1

Assertion

Ref	Expression
alrimdv

Distinct variable groups:   ,   ,

Proof of Theorem alrimdv

Step	Hyp	Ref	Expression
1		ax-5 1671	. 2
2		ax-5 1671	. 2
3		alrimdv.1	. 2
4	1, 2, 3	alrimdh 1640	1

Syntax hints:  ->wi 4  A.wal 1368

This theorem is referenced by:  axc9lem2  2000  zfpair  4646  fliftfun  6136  isofrlem  6162  funcnvuni  6663  f1oweALT  6694  findcard  7686  findcard2  7687  dfac5lem4  8433  dfac5  8435  zorn2lem4  8805  genpcl  9314  psslinpr  9337  ltaddpr  9340  ltexprlem3  9344  suplem1pr  9358  uzwo  11056  uzwoOLD  11057  seqf1o  12004  ramcl  14248  alexsubALTlem3  20020  truniALT  32091  ggen31  32096  onfrALTlem2  32097  gen21  32184  gen22  32187  ggen22  32188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1592  ax-4 1603  ax-5 1671