Theorem exbii 1027

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

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

This theorem is referenced by:  2exbii 1028  3exbi 1029  exancom 1030  19.29 1047  excom13 1074  exrot4 1076  eeor 1096  equsex 1135  19.12vv 1284  19.41vv 1288  19.41vvv 1289  exdistr 1291  exdistr2 1293  3exdistr 1294  4exdistr 1295  eeeanv 1306  ee4anv 1307  2sb5 1317  2sb5rf 1320  sbel2x 1327  exsb 1332  2exsb 1333  sb8eu 1367  eu1 1369  eu2 1373  moanim 1404  euan 1405  2moswap 1421  2exeu 1423  2eu1 1426  exists1 1434  clelab 1557  clabel 1558  sbabel 1560  rexbii2 1648  r2ex 1667  r19.29 1732  r19.41v 1739  r19.43 1741  isset 1789  rexv 1796  ceqsex2 1811  gencbvex 1813  vtocl2 1818  vtocl3 1819  cla42gv 1840  ceqsrexv 1861  euxfr 1898  reu3 1902  reu6 1903  2reuswap 1908  sbccomglem 1959  nss 2084  abn0 2261  pssnel 2302  snprc 2414  eusn 2416  elunirab 2482  unipr 2483  uniun 2487  uniin 2488  uni0b 2491  dfiun2g 2554  iinss 2568  iunid 2571  iunn0 2575  iunxsn 2580  iunxun 2582  cbvopab2v 2645  unopab 2647  axrep1 2662  axrep4 2665  axrep5 2666  zfrep4 2669  axsep 2670  zfnuleu 2675  axnul2 2676  nvelv 2681  inex1 2684  axpow 2711  pwex 2713  nssss 2732  zfpair 2745  zfpair2 2748  eqvinop 2758  copsexg 2759  opabid 2772  opabn0 2786  dfid3 2799  axun 2831  uniex2 2833  uniuni 2843  reusn 2855  onminex 2983  elxp2 3166  opelxp 3176  opelcog 3247  cnvco 3257  cnvuni 3258  dfdm3 3259  dfrn2 3260  dfrn3 3261  dfdm4 3262  eldm2 3265  dmun 3274  dmin 3275  dmuni 3276  dmopab 3277  dmi 3283  elrn 3306  rnopab 3309  dmcoss 3314  dmcosseq 3316  dmres 3331  dfima2 3356  dfima3 3357  elima3 3361  imadmrn 3365  imai 3368  imasng 3375  elimasn 3377  args 3379  intirr 3390  elxp4 3402  elxp5 3403  rnuni 3408  ssrnres 3427  rninxp 3428  resco 3442  imaco 3443  rnco 3444  coi1 3452  coass 3454  dffun2 3467  dffun5 3470  imadif 3514  funimaexg 3515  fcoi1 3584  fcoi2 3585  f11o 3651  fv2 3659  fvopabn 3725  fvresex 3796  imaiun 3803  funiunfv 3805  abexssex 3811  abexex 3812  isomin 3838  iinon 3849  dfoprab2 3930  1st2val 4033  2nd2val 4034  2ndconst 4035  dfopab2 4051  dfoprab3 4052  oarec 4134  ec2 4202  erdmrn 4214  ecdmn0 4218  snec 4234  domen 4315  mapsnen 4364  xpsnen 4369  xpassen 4375  abfii2 4488  inf2 4532  axinf 4547  axinf2 4548  zfinf 4550  tz9.12lem3 4585  rankuni 4622  scott0 4641  cp 4646  aceq1 4653  aceq0 4654  aceq2 4655  aceq5lem1 4659  aceq5lem2 4660  aceq5lem3 4661  axac 4669  ac9s 4688  kmlem3 4691  kmlem14 4702  kmlem15 4703  kmlem16 4704  cflem 4828  cf0 4833  axpowndlem3 4874  zfcndrep 4889  zfcndun 4890  zfcndpow 4891  zfcndinf 4893  zfcndac 4894  prnmadd 5023  genpass 5035  1pr 5040  distrlem1pr 5050  ltexprlem1 5065  ltexprlem4 5068  reclem1pr 5079  reclem2pr 5080  suplem1pr 5084  suppsr3 5147  elreal 5173  2rexuz 6329  nnwof 6342  nnwos 6343  cbvsum 6875  isumshft 7090  isumshft2 7091  isumnn0nn 7093  isum0split 7103  infcvglem1 7107  efseq1ex 7199  dfef2 7200  efseq0ex 7204  efclt 7205  efcvg 7207  efcvgfsum 7208  reefcl 7210  eirrlem4 7284  acdcALT 7389  infxpidmlem9 7454  isbasis2g 7505  tgval2t 7510  tgval3t 7518  tgss3t 7531  basgent 7533  subtop 7539  ismet 7685  cncfmet 7792  bcthlem14 7894  bcthlem31 7911  isgrp 7923  axgroth2 8630  axgroth3 8631  axgroth4 8632  grothprim 8635  19.41vvvv 8695  eeeeanv 8696  ntunte 8699  abfi 8708  ficli 8727  hmeogrp 8776  isalg 8847  algi 8854  osumlem5 9713  nmcopexlem1 10080  nmcfnexlem1 10109

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-gen 955

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

Copyright terms: Public domain