Theorem ralbiia 3082

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 271	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralbii2 3080	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-ral 3053

This theorem is referenced by:  ralbii  3084  ralanid  3086  poinxp  5715  soinxp  5716  seinxp  5718  dffun8  6530  funcnv3  6572  fncnv  6575  fnres  6629  fvreseq0  6994  isoini2  7297  smores  8296  tfr3ALT  8345  resixp  8885  ixpfi2  9264  marypha1lem  9350  ac5num  9960  acni2  9970  acndom  9975  dfac4  10046  brdom7disj  10455  brdom6disj  10456  fpwwe2lem7  10562  axgroth6  10753  rabssnn0fi  13923  lo1res  15496  isprm5  16648  prmreclem2  16859  tsrss  18526  gass  19247  efgval2  19670  efgsres  19684  isdomn2  20661  isdomn2OLD  20662  acsfn1p  20749  islinds2  21785  isclo  23048  ptclsg  23576  ufilcmp  23993  cfilres  25269  ovolgelb  25454  volsup2  25579  vitali  25587  itg1climres  25688  itg2seq  25716  itg2monolem1  25724  itg2mono  25727  itg2i1fseq  25729  itg2cn  25737  ellimc2  25851  rolle  25967  lhop1  25992  itgsubstlem  26028  tdeglem4  26038  mpodvdsmulf1o  27177  dvdsmulf1o  27179  dchrelbas2  27221  selbergsb  27559  axcontlem2  29056  dfconngr1  30281  hodsi  31869  ho01i  31922  ho02i  31923  lnopeqi  32102  nmcopexi  32121  nmcfnexi  32145  cnlnadjlem3  32163  cnlnadjlem5  32165  leop3  32219  pjssposi  32266  largei  32361  mdsl2i  32416  mdsl2bi  32417  elat2  32434  dmdbr5ati  32516  cdj3lem3b  32534  subfacp1lem3  35404  dfso3  35942  phpreu  37884  ptrecube  37900  mblfinlem1  37937  voliunnfl  37944  ralrnmo  38641  raldmqsmo  38643  disjressuc2  38691  fimgmcyc  42933  alephiso2  43943  ntrneiel2  44471  wfac8prim  45387  ismbl3  46373  ismbl4  46380  sge0lefimpt  46810  sbgoldbalt  48170