Theorem exbii 1047

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 1046	. 2 |- (A.x(ph <-> ps) -> (E.xph <-> E.xps))
2		exbii.1	. 2 |- (ph <-> ps)
3	1, 2	mpg 983	1 |- (E.xph <-> E.xps)

Syntax hints:   <-> wb 146  E.wex 977

This theorem is referenced by:  2exbii 1048  3exbi 1049  exancom 1050  19.29 1067  excom13 1094  exrot4 1096  eeor 1116  equsex 1148  19.12vv 1297  19.41vv 1301  19.41vvv 1302  exdistr 1304  exdistr2 1306  3exdistr 1307  4exdistr 1308  eeeanv 1319  ee4anv 1320  2sb5 1330  2sb5rf 1333  sbel2x 1340  exsb 1345  2exsb 1346  sb8eu 1383  eu1 1385  eu2 1389  moanim 1420  euan 1421  2moswap 1437  2exeu 1439  2eu1 1442  exists1 1450  clelab 1573  clabel 1574  sbabel 1576  rexbii2 1664  r2ex 1683  r19.29 1748  r19.41v 1755  r19.43 1757  isset 1805  rexv 1812  ceqsex2 1827  gencbvex 1829  vtocl2 1834  vtocl3 1835  cla42gv 1856  cla43gv 1858  ceqsrexv 1880  euxfr 1917  reu3 1921  reu6 1922  2reuswap 1927  sbccomglem 1978  nss 2103  abn0 2280  pssnel 2321  snprc 2433  eusn 2436  elunirab 2504  unipr 2505  uniun 2509  uniin 2510  uni0b 2513  dfiun2g 2576  iinss 2590  iunid 2593  iunn0 2597  iunxsn 2602  iunxun 2604  cbvopab2v 2667  unopab 2669  axrep1 2684  axrep4 2687  axrep5 2688  zfrep4 2691  axsep 2692  zfnuleu 2697  axnul2 2698  nvelv 2703  inex1 2706  axpow 2733  pwex 2735  nssss 2754  zfpair 2767  zfpair2 2770  eqvinop 2781  copsexg 2782  opabid 2799  opabn0 2813  dfid3 2826  axun 2858  uniex2 2860  uniuni 2870  reusn 2882  onminex 3010  elxp2 3193  opelxp 3204  relop 3265  opelcog 3279  cnvco 3289  cnvuni 3290  dfdm3 3291  dfrn2 3292  dfrn3 3293  dfdm4 3294  eldm2 3297  dmun 3306  dmin 3307  dmuni 3308  dmopab 3309  dmi 3315  elrn 3336  rnopab 3339  dmcoss 3347  dmcosseq 3349  dmres 3364  dfima2 3389  dfima3 3390  elima3 3394  imadmrn 3398  imai 3401  imasng 3408  elimasn 3410  args 3412  intirr 3427  elxp4 3439  elxp5 3440  rnuni 3445  ssrnres 3467  rninxp 3468  resco 3486  imaco 3487  rnco 3488  coi1 3496  coass 3498  dffun2 3512  dffun5 3515  imadif 3560  funimaexg 3561  fcoi1 3630  fcoi2 3631  f11o 3697  fv2 3705  fvopabn 3771  fvresex 3842  imaiun 3849  funiunfv 3851  abexssex 3857  abexex 3858  isomin 3884  iinon 3895  dfoprab2 3976  1st2val 4079  2nd2val 4080  2ndconst 4081  dfopab2 4097  dfoprab3 4098  oarec 4180  dfec2 4248  erdmrn 4260  ecdmn0 4264  snec 4280  domen 4361  mapsnen 4410  xpsnen 4415  xpassen 4421  abfii2 4536  inf2 4580  axinf 4595  axinf2 4596  zfinf 4598  tz9.12lem3 4633  rankuni 4670  scott0 4689  cp 4694  aceq1 4701  aceq0 4702  aceq2 4703  aceq5lem1 4707  aceq5lem2 4708  aceq5lem3 4709  axac 4717  ac9s 4736  kmlem3 4739  kmlem14 4750  kmlem15 4751  kmlem16 4752  cflem 4877  cf0 4882  axpowndlem3 4923  zfcndrep 4938  zfcndun 4939  zfcndpow 4940  zfcndinf 4942  zfcndac 4943  prnmadd 5072  genpass 5084  1pr 5089  distrlem1pr 5099  ltexprlem1 5114  ltexprlem4 5117  reclem1pr 5128  reclem2pr 5129  suplem1pr 5133  suppsr3 5196  elreal 5222  2rexuz 6378  nnwof 6391  nnwos 6392  cbvsum 6924  isumshft 7139  isumshft2 7140  isumnn0nn 7142  isum0split 7152  infcvglem1 7156  efseq1ex 7248  dfef2 7249  efseq0ex 7253  efclt 7254  efcvg 7256  efcvgfsum 7257  reefcl 7259  eirrlem4 7333  acdcALT 7438  infxpidmlem9 7503  isbasis2g 7554  tgval2t 7559  tgval3t 7567  tgss3t 7580  basgent 7582  subtop 7588  ismet 7737  cncfmet 7844  bcthlem14 7946  bcthlem31 7963  isgrp 7975  spwval2 8577  axgroth2 8717  axgroth3 8718  axgroth4 8719  grothprim 8722  osumlem5 9499  nmcopexlem1 9866  nmcfnexlem1 9895  19.41vvvv 10335  eeeeanv 10336  ntunte 10340  abfi 10349  ficli 10368  hmeogrp 10425  isalg 10497  algi 10504

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain