Theorem exbii 1083

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

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

This theorem is referenced by:  2exbii 1084  3exbii 1085  exancom 1086  19.29 1103  excom13 1130  exrot4 1132  eeor 1152  equsex 1185  19.12vv 1335  19.41vv 1339  19.41vvv 1340  exdistr 1342  exdistr2 1344  3exdistr 1345  4exdistr 1346  eeeanv 1357  ee4anv 1358  2sb5 1368  2sb5rf 1371  sbel2x 1378  exsb 1383  2exsb 1384  sb8eu 1423  eu1 1425  eu2 1429  moanim 1460  euan 1461  2moswap 1478  2exeu 1480  2eu1 1483  exists1 1492  clelab 1618  clabel 1619  sbabel 1621  rexbii2 1710  r2ex 1729  r19.29 1794  r19.41v 1801  r19.43 1803  isset 1852  rexv 1859  ceqsex2 1874  gencbvex 1876  vtocl2 1881  vtocl3 1882  cla42gv 1903  cla43gv 1905  ceqsrexv 1927  euxfr 1965  reu3 1969  reu6 1970  2reuswap 1975  sbc8g 1996  sbccomglem 2030  nss 2157  abn0 2335  pssnel 2376  snprc 2488  eusn 2491  elunirab 2562  unipr 2563  uniun 2567  uniin 2568  uni0b 2571  dfiun2g 2635  iinss 2649  iunn0 2657  iunxsn 2662  iunxun 2664  cbvopab2v 2728  unopab 2730  axrep1 2745  axrep4 2748  axrep5 2749  zfrep4 2752  axsep 2753  zfnuleu 2758  axnul2 2759  vprc 2764  inex1 2767  axpow 2795  pwex 2797  nssss 2817  zfpair 2830  zfpair2 2833  eqvinop 2844  copsexg 2845  opabid 2863  opabn0 2878  dfid3 2890  axun 2921  uniex2 2923  uniuni 2935  reusn 2947  onminex 3075  elxp2 3258  opelxp 3271  elvvv 3287  relop 3338  opelco2g 3353  cnvco 3364  cnvuni 3365  dfdm3 3366  dfrn2 3367  dfrn3 3368  dfdm4 3369  eldm2 3372  dmun 3381  dmin 3382  dmuni 3383  dmopab 3384  dmi 3388  elrn 3410  rnopab 3413  dmcoss 3423  dmcosseq 3425  dmres 3441  dfima2 3468  dfima3 3469  elima3 3473  imadmrn 3477  imai 3480  imasng 3487  elimasn 3489  args 3491  intirr 3504  rnuni 3515  ssrnres 3537  rninxp 3538  elxp4 3555  elxp5 3556  dfco2 3568  resco 3573  imaco 3574  rnco 3575  coiun 3578  coi1 3584  coass 3586  dffun2 3601  dffun5 3604  imadif 3649  funimaexg 3650  fcoi1 3720  fcoi2 3721  f11o 3788  fv2 3796  fvopabn 3862  fvresex 3933  imaiun 3940  funiunfv 3942  abexssex 3948  abexex 3949  isomin 3975  iinon 3986  dfoprab2 4067  dfopab2 4190  dfoprab3 4191  oarec 4280  dfec2 4348  erdmrn 4360  ecdmn0 4364  ecdmn0OLD 4365  uniqs 4383  snec 4384  domen 4466  mapsnen 4516  xpsnen 4522  xpassen 4528  abfii2 4646  inf2 4694  axinf 4709  axinf2 4710  zfinf 4712  tz9.12lem3 4747  rankuni 4784  scott0 4803  cp 4808  aceq1 4815  aceq0 4816  aceq2 4817  aceq5lem1 4821  aceq5lem2 4822  aceq5lem3 4823  axac 4831  ac9s 4850  kmlem3 4853  kmlem14 4864  kmlem15 4865  kmlem16 4866  cflem 4994  cf0 4999  axpowndlem3 5040  zfcndrep 5055  zfcndun 5056  zfcndpow 5057  zfcndinf 5059  zfcndac 5060  prnmadd 5189  genpass 5201  1pr 5206  distrlem1pr 5216  ltexprlem1 5231  ltexprlem4 5234  reclem1pr 5245  reclem2pr 5246  suplem1pr 5250  suppsr3 5313  elreal 5339  2rexuz 6506  nnwof 6519  nnwos 6520  cbvsumi 7109  isumshfti 7327  isumshft2i 7328  isumnn0nn 7330  isum0spliti 7340  infcvglem1 7344  efseq1ex 7429  dfef2i 7430  efseq0ex 7434  efcl 7435  efcvg 7437  efcvgfsum 7438  reefcli 7440  eirrlem4 7515  acdcALT 7621  infxpidmlem9 7685  isbasis2g 7736  tgval2 7741  tgval3 7749  tgss3 7762  basgen 7764  subtop 7768  ismet 7918  cncfmet 8025  bcthlem14 8132  bcthlem31 8149  isgrp 8161  spwval2 8772  axgroth2 8897  axgroth3 8898  axgroth4 8899  grothprim 8902  osumlem5 9702  nmcopexlem1 10068  nmcfnexlem1 10097  19.41vvvv 10557  eeeeanv 10558  ntunte 10561  abfi 10571  ficli 10590  hmeogrp 10674  rcfpfillem3 10718  isalg 10788  algi 10795

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-4 1005  ax-5o 1007

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

Copyright terms: Public domain