Theorem exbii 1087

Description: Inference adding existential quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
exbii.1	|- (ph <-> ps)

Assertion

Ref	Expression
exbii	|- (E.xph <-> E.xps)

Proof of Theorem exbii

Step	Hyp	Ref	Expression
1		19.18 1086	. 2 |- (A.x(ph <-> ps) -> (E.xph <-> E.xps))
2		exbii.1	. 2 |- (ph <-> ps)
3	1, 2	mpg 1022	1 |- (E.xph <-> E.xps)

Syntax hints:   <-> wb 144  E.wex 1016

This theorem is referenced by:  2exbii 1088  3exbii 1089  exancom 1090  19.29 1107  excom13 1134  exrot4 1136  eeor 1156  equsex 1189  19.12vv 1340  19.41vv 1344  19.41vvv 1345  exdistr 1347  exdistr2 1349  3exdistr 1350  4exdistr 1351  eeeanv 1362  ee4anv 1363  2sb5 1374  2sb5rf 1377  sbel2x 1384  exsb 1389  2exsb 1390  sb8eu 1429  eu1 1431  eu2 1435  moanim 1466  euan 1467  2moswap 1484  2exeu 1486  2eu1 1489  exists1 1498  clelab 1624  clabel 1625  sbabel 1627  rexbii2 1718  r2ex 1737  r19.29 1802  r19.41v 1809  r19.43 1811  isset 1860  rexv 1867  ceqsex2 1882  gencbvex 1884  vtocl2 1889  vtocl3 1890  cla42gv 1911  cla43gv 1913  ceqsrexv 1935  euxfr 1973  reu3 1977  reu6 1978  2reuswap 1983  sbc8g 2004  sbccomglem 2038  nss 2165  abn0 2343  pssnel 2384  snprc 2504  eusn 2507  elunirab 2580  unipr 2581  uniun 2586  uniin 2587  uni0b 2590  dfiun2g 2654  iinss 2668  iunn0 2676  iunxsn 2682  iunxun 2684  cbvopab2v 2751  unopab 2753  axrep1 2768  axrep4 2771  axrep5 2772  zfrep4 2775  axsep 2776  zfnuleu 2781  axnul2 2782  vprc 2787  inex1 2790  axpweq 2817  zfpow 2819  axpow2 2820  axpow3 2821  pwex 2823  nssss 2841  zfpair 2853  zfpair2 2856  eqvinop 2867  copsexg 2868  opabid 2887  opabn0 2902  dfid3 2914  zfun 3090  uniex2 3092  uniuni 3104  reusn 3115  onminex 3164  elxp2 3284  opelxp 3297  elvvv 3314  relop 3365  opelco2g 3380  cnvco 3391  cnvuni 3392  dfdm3 3393  dfrn2 3394  dfrn3 3395  dfdm4 3396  eldm2 3399  dmun 3408  dmin 3409  dmuni 3410  dmopab 3411  dmi 3415  elrn 3437  rnopab 3440  dmcoss 3450  dmcosseq 3452  dmres 3470  dfima2 3497  dfima3 3498  elima3 3502  imadmrn 3506  imai 3509  imasng 3516  elimasn 3518  args 3520  intirr 3533  rnuni 3544  ssrnres 3566  rninxp 3567  elxp4 3585  elxp5 3586  dfco2 3598  coundi 3600  coundir 3601  resco 3603  imaco 3604  rnco 3605  coiun 3608  coi1 3614  coass 3616  dffun2 3631  dffun5 3634  imadif 3679  funimaexg 3681  iunfopab 3719  fcoi1 3752  fcoi2 3753  f11o 3823  fv2 3831  fvopabn 3897  fvresex 3971  imaiun 3978  funiunfv 3980  abexssex 3986  abexex 3987  isomin 4013  dfoprab2 4050  dfopab2 4173  dfoprab3 4174  fparlem3 4201  fparlem4 4202  fsplit 4204  iinon 4208  onopriun 4211  oarec 4332  dfec2 4404  erdmrn 4416  ecdmn0 4420  uniqs 4436  snec 4437  domen 4520  mapsnen 4570  xpsnen 4576  xpassen 4582  abfii2 4705  inf2 4753  zfinf 4768  axinf2 4769  zfinf2 4771  tz9.12lem3 4807  rankuni 4844  scott0 4863  cp 4868  aceq1 4875  aceq0 4876  aceq2 4877  aceq5lem1 4881  aceq5lem2 4882  aceq5lem3 4883  zfac 4891  ac9s 4910  kmlem3 4913  kmlem14 4924  kmlem15 4925  kmlem16 4926  cflem 5055  cf0 5060  axpowndlem3 5105  zfcndrep 5120  zfcndun 5121  zfcndpow 5122  zfcndinf 5124  zfcndac 5125  prnmadd 5254  genpass 5266  1pr 5271  distrlem1pr 5281  ltexprlem1 5296  ltexprlem4 5299  reclem1pr 5310  reclem2pr 5311  suplem1pr 5315  suppsr3 5378  elreal 5404  2rexuz 6573  nnwof 6586  nnwos 6587  cbvsumi 7189  isumshfti 7408  isumshft2i 7409  isumnn0nn 7411  isum0spliti 7421  infcvglem1 7425  efseq1ex 7511  dfef2i 7512  efseq0ex 7516  efcl 7517  efcvg 7519  efcvgfsum 7520  reefcli 7522  eirrlem4 7597  acdcALT 7708  infxpidmlem9 7772  isbasis2g 7824  tgval2 7829  tgval3 7837  tgss3 7850  basgen 7852  subtop 7858  ismet 8008  cncfmet 8116  bcthlem14 8223  bcthlem31 8240  isgrp 8254  spwval2 8915  axgroth2 9050  axgroth3 9051  axgroth4 9052  grothpw 9054  axgroth5 9055  grothprim 9057  osumlem5 9860  nmcopexlem1 10230  nmcfnexlem1 10259  19.41vvvv 10719  eeeeanv 10720  ntunte 10728  abfi 10737  ficli 10756  islatalg 10831  ismgm 10897  hmeogrp 11044  sbtpsines 11062  rcfpfillem3 11091  isalg 11175  algi 11181  cnvresima 11407  opncldf1 11454  compfipin0 11493  alexsublem3 11498  is1stc3 11530  isfne2 11542  isfne3 11543  neibastop2lem2 11581  neibastop2lem4 11583  isfbas2 11622  elfg 11633  extbas1 11641  filrn 11643  neifg 11644  filssufillem 11655  ufileu 11658  hausfillim 11685  gapm 11784  sbmo 11787  opabex3 11806  oprabopabf 11807  firnfi3 11830  sdc 11877  fsumleisumi 11889  sstotbnd 11992  heiborlem1 12011

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017

Copyright terms: Public domain