Theorem ralbii 2536

Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

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

Proof of Theorem ralbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	ralbidv 2530	. 2 ⊢ (⊤ → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1404	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 105  ⊤wtru 1396  ∀wral 2508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-ral 2513

This theorem is referenced by:  2ralbii  2538  ralinexa  2557  r3al  2574  r19.26-2  2660  r19.26-3  2661  ralbiim  2665  r19.28av  2667  ralnex2  2670  ralrot3  2696  cbvral2vw  2776  cbvral2v  2778  cbvral3v  2780  sbralie  2783  ralcom4  2822  reu8  2999  2reuswapdc  3007  r19.12sn  3732  eqsnm  3832  uni0b  3912  uni0c  3913  ssint  3938  iuniin  3974  iuneq2  3980  iunss  4005  ssiinf  4014  iinab  4026  iindif2m  4032  iinin2m  4033  iinuniss  4047  sspwuni  4049  iinpw  4055  dftr3  4185  trint  4196  bnd2  4256  reusv3  4550  reg2exmidlema  4625  setindel  4629  ordsoexmid  4653  zfregfr  4665  tfi  4673  tfis2f  4675  ssrel2  4808  reliun  4839  xpiindim  4858  ralxpf  4867  dfse2  5100  rninxp  5171  dminxp  5172  cnviinm  5269  cnvpom  5270  cnvsom  5271  dffun9  5346  funco  5357  funcnv3  5382  fncnv  5386  funimaexglem  5403  fnres  5439  fnopabg  5446  mptfng  5448  fintm  5510  f1ompt  5785  idref  5879  dff13f  5893  foov  6151  tfr1onlemaccex  6492  tfrcllembxssdm  6500  tfrcllemaccex  6505  oacl  6604  ixpeq2  6857  ixpin  6868  ixpiinm  6869  infmoti  7191  acfun  7385  exmidontriimlem1  7399  exmidontriimlem3  7401  ccfunen  7446  cc2  7449  cc4f  7451  cc4n  7453  cauappcvgprlemladdrl  7840  axcaucvglemres  8082  axpre-suploc  8085  dfinfre  9099  suprzclex  9541  supinfneg  9786  infsupneg  9787  infssuzex  10448  cvg1nlemcau  11490  cvg1nlemres  11491  rexfiuz  11495  recvguniq  11501  resqrexlemglsq  11528  resqrexlemsqa  11530  resqrexlemex  11531  clim0  11791  mertenslem2  12042  bezoutlemmain  12514  ennnfoneleminc  12977  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemr  12989  ctinfom  12994  isnsg2  13735  isbasis2g  14713  tgval2  14719  ntreq0  14800  lmres  14916  eltx  14927  suplociccreex  15292  lgseisenlem2  15744  decidi  16117  nninfsellemqall  16340  nninfomni  16344  trirec0xor  16372