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

Theorem eeanv 1913
 Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
Assertion
Ref Expression
eeanv (xy(φ ψ) ↔ (xφ yψ))
Distinct variable groups:   φ,y   ψ,x
Allowed substitution hints:   φ(x)   ψ(y)

Proof of Theorem eeanv
StepHypRef Expression
1 nfv 1619 . 2 yφ
2 nfv 1619 . 2 xψ
31, 2eean 1912 1 (xy(φ ψ) ↔ (xφ yψ))
 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-7 1734  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:  eeeanv  1914  ee4anv  1915  pm11.07  2115  2eu4  2287  cgsex2g  2891  cgsex4g  2892  vtocl2  2910  spc2egv  2941  opkelcokg  4261  sikexlem  4295  ncfinlower  4483  sfin112  4529  sfinltfin  4535  copsex2t  4608  copsex2g  4609  opeqexb  4620  opelxp  4811  xpnz  5045  dfxp2  5113  fununi  5160  1stfo  5505  2ndfo  5506  brtxp  5783  dmtxp  5802  dmpprod  5840  pw1fnf1o  5855  entr  6038  fundmen  6043  unen  6048  xpen  6055  muccl  6132  muccom  6134  ncaddccl  6144  ncdisjeq  6148  tcdi  6164  ce0addcnnul  6179  ce0nnulb  6182  ceclb  6183  sbthlem3  6205  dflec3  6221  nclenc  6222  lenc  6223  tc11  6228  ce2le  6233  muc0or  6252  fnfrec  6320
 Copyright terms: Public domain W3C validator