Theorem ralbii 2127

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

Hypothesis

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

Assertion

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

Proof of Theorem ralbii

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	ralbid 2121	. 2 |- ((ph <-> ph) -> (A.x e. A ph <-> A.x e. A ps))
6	1, 5	ax-mp 7	1 |- (A.x e. A ph <-> A.x e. A ps)

Syntax hints:   <-> wb 163  A.wral 2105

This theorem is referenced by:  2ralbii 2129  ralinexa 2143  hbra2 2148  r3al 2151  r19.26-2 2221  r19.28av 2226  r19.32v 2230  r19.35 2231  cbvral2v 2283  cbvral3v 2284  ralcom4 2310  ralcom4OLD 2311  reu8 2448  sbralie 2453  r19.12sn 3093  eqsn 3143  uni0b 3203  uni0c 3204  ssint 3232  iuniin 3264  iuniinOLD 3265  iuneq2 3273  dfiin2 3287  iunss 3291  iunssOLD 3292  ssiin 3302  ssiinOLD 3303  iinab 3317  iinun2 3321  iindif2 3324  iinuni 3330  sspwuni 3333  iinpw 3336  dftr3 3415  truni 3425  trint 3426  dffr2OLD 3628  eufromeq2 3829  eufromeq6 3833  dfwe2 3861  dfwe2OLD 3862  tfis2f 3939  rexxp 4042  ralxpf 4043  rexxpf 4044  reliun 4101  asymref2 4310  rninxp 4355  rninxpOLD 4356  dminxp 4357  cnvpo 4427  dffun9 4450  funcnv3 4476  fncnv 4479  fnopab2g 4547  fint 4591  fintOLD 4592  funimass4 4722  funconstss 4781  fopab2 4796  dff13f 4851  fooprv 4967  dfrdg2 5141  tz7.48lem 5164  tz7.49 5168  oeordi 5262  oaabs 5309  ixpeq2 5414  xpmapenlem4 5593  ordiso 5683  ordtypelem4 5687  ordtypelem7 5690  zfinf2 5732  zfregs2 5755  rankc1 5816  cp 5852  bnd2 5854  aceq1 5891  aceq2 5893  ac6s2 5920  ac6sf 5922  ac6s4 5923  ac9s 5926  kmlem7 5933  kmlem12 5938  kmlem13 5939  kmlem15 5941  zorn2lem4 5953  zorn2lem6 5955  zorn2lem7 5956  zorn 5959  brdom7disj 5966  brdom6disj 5967  unidom 5970  dfinfmr 7276  infmsup 7277  xrsupsslem 7285  xrinfmsslem 7286  infmxrcl 7295  uzwo3lem2 7430  fzshftral 7701  cau3iri 8167  cau5i 8171  cvg3i 8175  csbfsum 8287  fsumrev 8289  fsumshft 8291  clm1i 8337  clmnnsi 8344  climshfti 8364  climresi 8365  caucvgi 8423  isumcmpii 8476  infxpidmlem8 8828  isbasis2g 8881  tgval2 8887  tgss3 8908  basgen 8910  cctop 8922  clsval2 8961  ntreq0 8984  sncld 9064  lmbr2 9207  iscau2 9215  lmbrnns 9220  bcthlem7 9283  grpidinvlem3 9330  lnon0 9798  axgroth5 10132  grothpw 10134  axgroth4 10139  grothprim 10141  elghom 10195  hmeobc 10239  hausfillim 10303  adjsym 11396  cvbr2 11855  chpssati 11935  chrelat2i 11937  chrelat3 11943  chrelat4i 11945  mdsymlem8 11982  bnj51 12426  bnj1135 12935  bnj1366 13091  bnj1480 13157  bnj1481 13158  bnj82 13210  bnj92 13216  bnj114 13227  bnj539 13266  bnj540 13267  bnj580 13301  bnj978 13355  bnj1047 13393  bnj1128 13428  bnj1417 13530  bnj1421 13532  bnj1498 13562  gcdcllem1 13718  truniOLD 13792  trintOLD 13794  untuni 13797  r19.30 13817  setinds 13844  setinds2f 13845  elpotr 13847  dfon2lem7 13855  dfon2lem9 13857  wfis2fg 13919  frins2fg 13943  frxp 13951  soseq 13955  axfelem15 14045  negcmpprcal1 14275  negcmpprcal2 14276  r19.26t 14282  fopab2g 14485  dstr 14516  defse3 14614  clfsebs 14707  trinv 14759  vecax3 14798  altretoplem2 14996  altretop 14997  imonclem 15162  ismonc 15163  isepic 15173  tartarmap 15265  ordisoOLD 15374  ordtypelem4OLD 15378  ordtypelem7OLD 15381  opnnei 15417  compsub 15431  compfipin0 15436  alexsublem3 15439  is1stc3 15469  isfne2 15481  limfilcf 15587  cnfillim 15590  flimfcn 15603  isfclus 15606  fcluscn 15619  fclsfcn 15632  inixp 15722  ac6gf 15749  infmrlb 15765  infmrgelb 15766  wofi 15770  fsumleisumi 15826  caures 15852  bfp 16009  iscring2 16146  n0el 16248  blkssatm 16289  zfregs2VD 16665  lubid 16807  glb0 16920  hlrelat1 17049  hlrelat2 17052  grpidinvlem3NEW 17111  ispsubsp2 17227

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-ral 2109

Copyright terms: Public domain