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-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
This theorem is referenced by:  exdistr  1906  19.42vv  1907  19.42vvv  1908  4exdistr  1911  cbvex2  2005  2sb5  2112  2sb5rf  2117  rexcom4a  2880  ceqsex2  2896  reuind  3040  2reu5lem3  3044  sbccomlem  3117  elpw1  4145  eluni1g  4173  opkelopkabg  4246  otkelins2kg  4254  eqvinop  4607  setconslem6  4737  dmopabss  4917  dmopab3  4918  dmcosseq  4974  coass  5098  dmoprab  5575  dmoprabss  5576  fnoprabg  5586  mptpreima  5683  dmmpt  5684  brsnsi2  5777  oqelins4  5795  addcfnex  5825  lecex  6116  ceex  6175  nmembers1lem1  6269  dmfrec  6317
  Copyright terms: Public domain W3C validator