Theorem ralbiia 1676

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

Hypothesis

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

Assertion

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

Proof of Theorem ralbiia

Step	Hyp	Ref	Expression
1		ralbiia.1	. . 3 |- (x e. A -> (ph <-> ps))
2	1	pm5.74i 586	. 2 |- ((x e. A -> ph) <-> (x e. A -> ps))
3	2	ralbii2 1674	1 |- (A.x e. A ph <-> A.x e. A ps)

Syntax hints:   -> wi 3   <-> wb 146   e. wcel 960  A.wral 1648

This theorem is referenced by:  funcnv3 3564  fncnv 3567  fvreseq 3805  aceq4 4744  brdom7disj 4814  brdom6disj 4815  iundom 4822  cau2 6913  clmnns 7084  climres 7105  climshft2 7106  isumnn0nna 7208  isummulc1a 7214  cvgratlem3ALT 7249  cvgratlem3 7252  negfcncf 7269  efaddlem27 7364  metreslem 7819  lmbrnns 7939  lmcvgnns 7940  hods 9696  ho01 9749  ho02 9750  lnopeq 9928  nmcopexlem2 9947  lnopcon 9958  nmcfnexlem2 9976  lnfncon 9985  cnlnadjlem3 9997  cnlnadjlem4 9998  cnlnadjlem5 9999  leop3t 10053  pjsspos 10095  large 10189  mdsl2 10244  mdsl2b 10245  elat2 10262  dmdbr5at 10344  cdj3lem3b 10362

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1652

Copyright terms: Public domain