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

Theorem r19.41v 2764
Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 17-Dec-2003.)
Assertion
Ref Expression
r19.41v (x A (φ ψ) ↔ (x A φ ψ))
Distinct variable group:   ψ,x
Allowed substitution hints:   φ(x)   A(x)

Proof of Theorem r19.41v
StepHypRef Expression
1 nfv 1619 . 2 xψ
21r19.41 2763 1 (x A (φ ψ) ↔ (x A φ ψ))
Colors of variables: wff setvar class
Syntax hints:  wb 176   wa 358  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-rex 2620
This theorem is referenced by:  r19.42v  2765  3reeanv  2779  reuind  3039  iuncom4  3976  dfiun2g  3999  iunxiun  4048  elpw12  4145  pw1in  4164  imacok  4282  unipw1  4325  dfaddc2  4381  addcass  4415  ltfinex  4464  ncfinlowerlem1  4482  dfevenfin2  4512  dfoddfin2  4513  nnpweqlem1  4522  vfinspss  4551  vfinncsp  4554  phialllem1  4616  setconslem6  4736  xpiundi  4817  xpiundir  4818  elimapw1  4944  elimapw12  4945  elimapw13  4946  imaco  5086  coiun  5090  abrexco  5463  imaiun  5464  isomin  5496  isoini  5497  xpassen  6057  enpw1pw  6075
  Copyright terms: Public domain W3C validator