Theorem rexbii 2128

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

Hypothesis

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

Assertion

Ref	Expression
rexbii	|- (E.x e. A ph <-> E.x e. A ps)

Proof of Theorem rexbii

Step	Hyp	Ref	Expression
1		biid 187	. 2 |- (ph <-> ph)
2	1	hbth 1348	. . 3 |- ((ph <-> ph) -> A.x(ph <-> ph))
3		ralbii.1	. . . 4 |- (ph <-> ps)
4	3	a1i 8	. . 3 |- ((ph <-> ph) -> (ph <-> ps))
5	2, 4	rexbid 2122	. 2 |- ((ph <-> ph) -> (E.x e. A ph <-> E.x e. A ps))
6	1, 5	ax-mp 7	1 |- (E.x e. A ph <-> E.x e. A ps)

Syntax hints:   <-> wb 163  E.wrex 2106

This theorem is referenced by:  2rexbii 2130  rexanali 2144  r19.29r 2229  r19.42v 2237  r19.43 2238  reeanOLD 2248  2ralor 2250  rexcom4 2312  rexcom4OLD 2313  ceqsrex2v 2395  reu7 2447  0el 2891  uni0b 3203  iuncom 3261  iuniin 3264  iuniinOLD 3265  iunrab 3299  iinssOLD 3305  iunn0 3315  iunn0OLD 3316  iunin2 3320  iundif2 3322  iunun 3328  iununi 3331  iununiOLD 3332  iunpwss 3337  inuni 3470  dffr2OLD 3628  dfepfr 3640  dfepfrOLD 3641  epfrc 3642  epfrcOLD 3643  sucel 3738  reuxfrd 3846  iunpw 3858  iunxpf 4045  cnvuni 4147  dfima3 4267  dffr3 4297  dminxp 4357  imaco 4403  coiun 4407  isarep1 4497  isarep1OLD 4498  iunfopabOLD 4543  abrexexlem2 4835  imaiun 4840  abrexex2 4847  elrnoprabg 5066  dfrdg2 5141  rdglem1 5145  tz7.49 5168  uniqs 5354  qsid 5360  ordtypelem4 5687  zfregcl 5697  zfreg 5698  zfreg2 5699  zfregs2 5755  ac6n 5919  kmlem7 5933  kmlem13 5939  numth2 5947  zorn2lem7 5956  zorn 5959  brdom7disj 5966  brdom6disj 5967  isinfcard 6035  ssxrOLD 6715  dfinfmr 7276  infmsup 7277  supxrre 7292  infmxrcl 7295  uzwo 7624  uzwoOLD 7625  nnwof 7628  cau3iri 8167  cbvsumi 8246  clmnnsi 8344  climunii 8358  climresi 8365  infcvglem1 8482  ivthlem6 8548  efaddlem27 8626  tgval2 8887  txbas 8933  blrn2 9119  lmbrnns 9220  lmcvgnns 9221  bcthlem33 9309  isgrp2i 9360  axgroth5 10132  grothpw 10134  axgroth4 10139  grothprim 10141  rexcom4a 10147  rexcom4b 10148  subsp 10244  hausfillim 10303  lpni 10347  axhcompl 10500  hhcmpl 10702  hlimuniii 10741  shne0i 11004  nmcopexlem1 11588  nmcopexlem2 11589  nmcfnexlem1 11617  nmcfnexlem2 11618  cdj3lem3b 12012  bnj4 12369  bnj41 12413  bnj163OLD 12490  bnj168 12496  bnj860 12793  bnj878 12805  bnj1159 12951  bnj1185 12967  bnj1194 12971  bnj1298 13043  bnj1437 13131  bnj1524 13177  bnj849 13318  bnj882 13320  bnj916 13332  bnj983 13357  bnj1398 13515  bnj1463 13550  ublbneg 13653  divalglem10 13705  divalgb 13707  dfon2lem9 13857  dffr4 13893  soseq 13955  axdenselem4 14022  axdenselem5 14023  axfelem11 14041  axfelem15 14045  axfelem16 14046  negcmpprcal2 14276  dstr 14516  iscst4 14522  cbvprodi 14662  imtr 14762  sallnei 14873  fictblem 15370  fictb 15371  ordtypelem4OLD 15378  compcov 15429  hscptsscld 15434  reconnlem1 15446  is1stc3 15469  locfincomp 15514  neibastop2lem3 15521  neibastop2lem4 15522  ist0-2 15539  isufil2 15565  ufileu 15573  limfilcf 15587  fcluscf 15612  flimfnfcls 15615  filnetlem2 15641  2ralorOLD 15655  rexcom4aOLD 15659  rexcom4bOLD 15660  3reeanv 15661  eropreu 15733  abrexex2g 15738  infmrlb 15765  infmrgelb 15766  wofi 15770  sdc 15811  fdc 15812  isbnd3 15941  heiborlem8 15962  heiborlem29 15983  ismrer1 16024  smprngpr 16200  isfldidl 16216  prter1 16282  prter2 16285  zfregs2VD 16665

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-rex 2110

Copyright terms: Public domain