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

Theorem 19.42v 1905
Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.42v (x(φ ψ) ↔ (φ xψ))
Distinct variable group:   φ,x
Allowed substitution hint:   ψ(x)

Proof of Theorem 19.42v
StepHypRef Expression
1 nfv 1619 . 2 xφ
2119.42 1880 1 (x(φ ψ) ↔ (φ xψ))
Colors of variables: wff setvar class
Syntax hints:  wb 176   wa 358  wex 1541
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-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545
This theorem is referenced by:  exdistr  1906  19.42vv  1907  19.42vvv  1908  4exdistr  1911  cbvex2  2005  2sb5  2112  2sb5rf  2117  rexcom4a  2879  ceqsex2  2895  reuind  3039  2reu5lem3  3043  sbccomlem  3116  elpw1  4144  eluni1g  4172  opkelopkabg  4245  otkelins2kg  4253  eqvinop  4606  setconslem6  4736  dmopabss  4916  dmopab3  4917  dmcosseq  4973  coass  5097  dmoprab  5574  dmoprabss  5575  fnoprabg  5585  mptpreima  5682  dmmpt  5683  brsnsi2  5776  oqelins4  5794  addcfnex  5824  lecex  6115  ceex  6174  nmembers1lem1  6267  dmfrec  6314
  Copyright terms: Public domain W3C validator