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

Theorem ralrimiva 2697
 Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
Hypothesis
Ref Expression
ralrimiva.1 ((φ x A) → ψ)
Assertion
Ref Expression
ralrimiva (φx A ψ)
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem ralrimiva
StepHypRef Expression
1 ralrimiva.1 . . 3 ((φ x A) → ψ)
21ex 423 . 2 (φ → (x Aψ))
32ralrimiv 2696 1 (φx A ψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∈ wcel 1710  ∀wral 2614 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619 This theorem is referenced by:  ralrimivvva  2707  rgen2  2710  rgen3  2711  nrexdv  2717  rabbidva  2850  ssrabdv  3345  ss2rabdv  3347  rgenz  3655  iuneq2dv  3990  ssofss  4076  findsd  4410  evenodddisj  4516  tfinnn  4534  vfinspss  4551  vfinspclt  4552  fun11iun  5305  eqfnfvd  5395  dff3  5420  dffo4  5423  foco2  5426  ffnfv  5427  ffvresb  5431  fconst2g  5452  fconstfv  5456  fmptd  5694  f1od  5726  extd  5923  refrd  5926  enmap2lem5  6067  enmap1lem5  6073  spacis  6288  nchoicelem12  6300  nchoicelem17  6305
 Copyright terms: Public domain W3C validator