Theorem biral 1223

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

Hypothesis

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

Assertion

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

Proof of Theorem biral

Step	Hyp	Ref	Expression
1		pm4.2 148	. 2 |- (ph <-> ph)
2	1	hbth 697	. . 3 |- ((ph <-> ph) -> A.x(ph <-> ph))
3		biral.1	. . . 4 |- (ph <-> ps)
4	3	a1i 7	. . 3 |- ((ph <-> ph) -> (ph <-> ps))
5	2, 4	birald 1217	. 2 |- ((ph <-> ph) -> (A.x e. A ph <-> A.x e. A ps))
6	1, 5	ax-mp 6	1 |- (A.x e. A ph <-> A.x e. A ps)

Syntax hints:   <-> wb 127  A.wral 1201

This theorem is referenced by:  bi2ral 1225  r3al 1240  r19.26-2 1290  r19.28av 1294  r19.32v 1297  r19.35 1298  cbvral2v 1336  ralcom4 1360  sbralie 1439  uni0b 1939  ssint 1980  iuniin 2001  iuneq2 2006  iunss 2017  ssiin 2024  iinun2 2031  iindif2 2033  iinuni 2036  iinpw 2038  dftr3 2045  dftr4 2046  dffr2 2171  dfwe2 2187  tfis2f 2246  reluni 2493  fint 2769  fopab2 2891  f1fvf 2917  tz7.48lem 2993  xpmapenlem4 3394  fiint 3445  zfinf 3474  cp 3547  bnd2 3549  aceq1 3552  aceq2 3554  ac6s2 3578  kmlem7 3586  kmlem11 3590  kmlem12 3591  kmlem15 3594  zornlem6 3608  zorn2 3612  uzwo3lem2 4615  infxpidmlem8 4940  cvbr2t 5715  chpssat 5756  chrelat2 5758  chrelat3t 5762  mdsymlem8 5783

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ral 1205

metamath.org