Theorem exbii 1050

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

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

This theorem is referenced by:  2exbii 1051  3exbi 1052  exancom 1053  19.29 1070  excom13 1097  exrot4 1099  eeor 1119  equsex 1151  19.12vv 1301  19.41vv 1305  19.41vvv 1306  exdistr 1308  exdistr2 1310  3exdistr 1311  4exdistr 1312  eeeanv 1323  ee4anv 1324  2sb5 1334  2sb5rf 1337  sbel2x 1344  exsb 1349  2exsb 1350  sb8eu 1389  eu1 1391  eu2 1395  moanim 1426  euan 1427  2moswap 1443  2exeu 1445  2eu1 1448  exists1 1456  clelab 1579  clabel 1580  sbabel 1582  rexbii2 1670  r2ex 1689  r19.29 1754  r19.41v 1761  r19.43 1763  isset 1811  rexv 1818  ceqsex2 1833  gencbvex 1835  vtocl2 1840  vtocl3 1841  cla42gv 1862  cla43gv 1864  ceqsrexv 1886  euxfr 1924  reu3 1928  reu6 1929  2reuswap 1934  sbccomglem 1985  nss 2110  abn0 2287  pssnel 2328  snprc 2440  eusn 2443  elunirab 2510  unipr 2511  uniun 2515  uniin 2516  uni0b 2519  dfiun2g 2582  iinss 2596  iunid 2599  iunn0 2603  iunxsn 2608  iunxun 2610  cbvopab2v 2673  unopab 2675  axrep1 2690  axrep4 2693  axrep5 2694  zfrep4 2697  axsep 2698  zfnuleu 2703  axnul2 2704  nvelv 2709  inex1 2712  axpow 2739  pwex 2741  nssss 2760  zfpair 2773  zfpair2 2776  eqvinop 2787  copsexg 2788  opabid 2806  opabn0 2820  dfid3 2832  axun 2863  uniex2 2865  uniuni 2876  reusn 2888  onminex 3016  elxp2 3199  opelxp 3210  relop 3271  opelcog 3286  cnvco 3296  cnvuni 3297  dfdm3 3298  dfrn2 3299  dfrn3 3300  dfdm4 3301  eldm2 3304  dmun 3313  dmin 3314  dmuni 3315  dmopab 3316  dmi 3322  elrn 3346  rnopab 3349  dmcoss 3359  dmcosseq 3361  dmres 3376  dfima2 3401  dfima3 3402  elima3 3406  imadmrn 3410  imai 3413  imasng 3420  elimasn 3422  args 3424  intirr 3437  elxp4 3449  elxp5 3450  rnuni 3455  ssrnres 3477  rninxp 3478  resco 3496  imaco 3497  rnco 3498  coi1 3506  coass 3508  dffun2 3522  dffun5 3525  imadif 3570  funimaexg 3571  fcoi1 3640  fcoi2 3641  f11o 3707  fv2 3715  fvopabn 3781  fvresex 3852  imaiun 3859  funiunfv 3861  abexssex 3867  abexex 3868  isomin 3894  iinon 3905  dfoprab2 3986  1st2val 4088  2nd2val 4089  2ndconst 4090  dfopab2 4106  dfoprab3 4107  oarec 4189  dfec2 4257  erdmrn 4269  ecdmn0 4273  snec 4289  domen 4370  mapsnen 4419  xpsnen 4424  xpassen 4430  abfii2 4545  inf2 4591  axinf 4606  axinf2 4607  zfinf 4609  tz9.12lem3 4644  rankuni 4681  scott0 4700  cp 4705  aceq1 4712  aceq0 4713  aceq2 4714  aceq5lem1 4718  aceq5lem2 4719  aceq5lem3 4720  axac 4728  ac9s 4747  kmlem3 4750  kmlem14 4761  kmlem15 4762  kmlem16 4763  cflem 4888  cf0 4893  axpowndlem3 4934  zfcndrep 4949  zfcndun 4950  zfcndpow 4951  zfcndinf 4953  zfcndac 4954  prnmadd 5083  genpass 5095  1pr 5100  distrlem1pr 5110  ltexprlem1 5125  ltexprlem4 5128  reclem1pr 5139  reclem2pr 5140  suplem1pr 5144  suppsr3 5207  elreal 5233  2rexuz 6391  nnwof 6404  nnwos 6405  cbvsum 6939  isumshft 7156  isumshft2 7157  isumnn0nn 7159  isum0split 7169  infcvglem1 7173  efseq1ex 7265  dfef2 7266  efseq0ex 7270  efclt 7271  efcvg 7273  efcvgfsum 7274  reefcl 7276  eirrlem4 7350  acdcALT 7455  infxpidmlem9 7520  isbasis2g 7572  tgval2t 7577  tgval3t 7585  tgss3t 7598  basgent 7600  subtop 7606  ismet 7758  cncfmet 7867  bcthlem14 7974  bcthlem31 7991  isgrp 8003  spwval2 8610  axgroth2 8733  axgroth3 8734  axgroth4 8735  grothprim 8738  osumlem5 9539  nmcopexlem1 9907  nmcfnexlem1 9936  19.41vvvv 10393  eeeeanv 10394  ntunte 10398  abfi 10407  ficli 10426  hmeogrp 10484  rcfpfillem3 10513  isalg 10569  algi 10576

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

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

Copyright terms: Public domain