Theorem reximia 2923

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)

Hypothesis

Ref	Expression
reximia.1

Assertion

Ref	Expression
reximia

Proof of Theorem reximia

Step	Hyp	Ref	Expression
1		rexim 2922	. 2
2		reximia.1	. 2
3	1, 2	mprg 2820	1

Syntax hints:  ->wi 4  e.wcel 1818  E.wrex 2808

This theorem is referenced by:  reximi  2925  iunpw  6614  tz7.49c  7130  fisup2g  7947  unwdomg  8031  trcl  8180  cfsmolem  8671  1idpr  9428  qmulz  11214  zq  11217  xrsupexmnf  11525  xrinfmexpnf  11526  caubnd2  13190  caurcvg  13499  caurcvg2  13500  caucvg  13501  txlm  20149  norm1exi  26168  chrelat2i  27284  xrofsup  27582  esumcvg  28092  wfrlem9  29351  ismblfin  30055  bnj168  33785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813