Theorem ralbiia 1673

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 584	. 2 |- ((x e. A -> ph) <-> (x e. A -> ps))
3	2	ralbii2 1671	1 |- (A.x e. A ph <-> A.x e. A ps)

Syntax hints:   -> wi 3   <-> wb 146   e. wcel 958  A.wral 1645

This theorem is referenced by:  funcnv3 3558  fncnv 3561  fvreseq 3799  aceq4 4734  brdom7disj 4804  brdom6disj 4805  iundom 4812  cau2 6913  clmnns 7084  climres 7105  climshft2 7106  isumnn0nna 7208  isummulc1a 7214  cvgratlem3ALT 7249  cvgratlem3 7252  negfcncf 7269  efaddlem27 7364  metreslem 7822  lmbrnns 7942  lmcvgnns 7943  hods 9701  ho01 9754  ho02 9755  lnopeq 9933  nmcopexlem2 9952  lnopcon 9963  nmcfnexlem2 9981  lnfncon 9990  cnlnadjlem3 10002  cnlnadjlem4 10003  cnlnadjlem5 10004  leop3t 10058  pjsspos 10100  large 10194  mdsl2 10249  mdsl2b 10250  elat2 10267  dmdbr5at 10349  cdj3lem3b 10367

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

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

Copyright terms: Public domain