NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  rexlimiv GIF version

Theorem rexlimiv 2732
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
rexlimiv.1 (x A → (φψ))
Assertion
Ref Expression
rexlimiv (x A φψ)
Distinct variable group:   ψ,x
Allowed substitution hints:   φ(x)   A(x)

Proof of Theorem rexlimiv
StepHypRef Expression
1 nfv 1619 . 2 xψ
2 rexlimiv.1 . 2 (x A → (φψ))
31, 2rexlimi 2731 1 (x A φψ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wcel 1710  wrex 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619  df-rex 2620
This theorem is referenced by:  rexlimiva  2733  rexlimivw  2734  rexlimivv  2743  r19.36av  2759  r19.44av  2767  r19.45av  2768  rexn0  3652  uniss2  3922  pwadjoin  4119  nnc0suc  4412  lefinlteq  4463  ssfin  4470  evennn  4506  oddnn  4507  sucoddeven  4511  evenodddisj  4516  eventfin  4517  oddtfin  4518  fnasrn  5417  ecoptocl  5996  mapsn  6026  dflec3  6221  lenc  6223  taddc  6229  ce0tb  6238  ce0lenc1  6239  ncfin  6247  nncdiv3  6277  nchoicelem1  6289  nchoicelem2  6290  nchoicelem12  6300
  Copyright terms: Public domain W3C validator