Theorem ralbiia 3108

Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)

Hypothesis

Ref	Expression
ralbiia.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralbiia	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralbiia

Step	Hyp	Ref	Expression
1		ralbiia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
2	1	pm5.74i 274	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralbii2 3106	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  ralbii  3110  ralanid  3112  poinxp  5740  soinxp  5741  seinxp  5743  dffun8  6565  funcnv3  6607  fncnv  6610  fnres  6663  fvreseq0  7034  isoini2  7343  smores  8344  tfr3ALT  8394  resixp  8943  ixpfi2  9320  marypha1lem  9406  ac5num  10042  acni2  10052  acndom  10057  dfac4  10128  brdom7disj  10537  brdom6disj  10538  fpwwe2lem7  10649  axgroth6  10840  rabssnn0fi  14052  lo1res  15648  isprm5  16802  prmreclem2  17013  tsrss  18681  gass  19429  efgval2  19852  efgsres  19866  isdomn2  20874  acsfn1p  20966  islinds2  22027  isclo  23313  ptclsg  23842  ufilcmp  24259  cfilres  25525  ovolgelb  25709  volsup2  25834  vitali  25842  itg1climres  25943  itg2seq  25971  itg2monolem1  25979  itg2mono  25982  itg2i1fseq  25984  itg2cn  25992  ellimc2  26106  rolle  26219  lhop1  26243  itgsubstlem  26277  tdeglem4  26287  mpodvdsmulf1o  27428  dvdsmulf1o  27430  dchrelbas2  27471  selbergsb  27809  axcontlem2  29408  dfconngr1  30654  hodsi  32242  ho01i  32295  ho02i  32296  lnopeqi  32475  nmcopexi  32494  nmcfnexi  32518  cnlnadjlem3  32536  cnlnadjlem5  32538  leop3  32592  pjssposi  32639  largei  32734  mdsl2i  32789  mdsl2bi  32790  elat2  32807  dmdbr5ati  32889  cdj3lem3b  32907  subfacp1lem3  35748  dfso3  36286  phpreu  38345  ptrecube  38356  mblfinlem1  38393  voliunnfl  38400  ralrnmo  39096  raldmqsmo  39098  disjressuc2  39146  fimgmcyc  43403  alephiso2  44385  ntrneiel2  44913  wfac8prim  45812  ismbl3  46801  ismbl4  46808  sge0lefimpt  47238  sbgoldbalt  48684