Theorem ralbii 2496

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 2490	. 2 ⊢ (⊤ → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1373	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 105  ⊤wtru 1365  ∀wral 2468

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-ral 2473

This theorem is referenced by:  2ralbii  2498  ralinexa  2517  r3al  2534  r19.26-2  2619  r19.26-3  2620  ralbiim  2624  r19.28av  2626  ralnex2  2629  ralrot3  2655  cbvral2vw  2729  cbvral2v  2731  cbvral3v  2733  sbralie  2736  ralcom4  2774  reu8  2948  2reuswapdc  2956  r19.12sn  3676  eqsnm  3773  uni0b  3852  uni0c  3853  ssint  3878  iuniin  3914  iuneq2  3920  iunss  3945  ssiinf  3954  iinab  3966  iindif2m  3972  iinin2m  3973  iinuniss  3987  sspwuni  3989  iinpw  3995  dftr3  4123  trint  4134  bnd2  4194  reusv3  4481  reg2exmidlema  4554  setindel  4558  ordsoexmid  4582  zfregfr  4594  tfi  4602  tfis2f  4604  ssrel2  4737  reliun  4768  xpiindim  4785  ralxpf  4794  dfse2  5022  rninxp  5093  dminxp  5094  cnviinm  5191  cnvpom  5192  cnvsom  5193  dffun9  5267  funco  5278  funcnv3  5300  fncnv  5304  funimaexglem  5321  fnres  5354  fnopabg  5361  mptfng  5363  fintm  5423  f1ompt  5691  idref  5781  dff13f  5795  foov  6047  tfr1onlemaccex  6377  tfrcllembxssdm  6385  tfrcllemaccex  6390  oacl  6489  ixpeq2  6742  ixpin  6753  ixpiinm  6754  infmoti  7061  acfun  7241  exmidontriimlem1  7255  exmidontriimlem3  7257  ccfunen  7298  cc2  7301  cc4f  7303  cc4n  7305  cauappcvgprlemladdrl  7691  axcaucvglemres  7933  axpre-suploc  7936  dfinfre  8948  suprzclex  9386  supinfneg  9631  infsupneg  9632  cvg1nlemcau  11034  cvg1nlemres  11035  rexfiuz  11039  recvguniq  11045  resqrexlemglsq  11072  resqrexlemsqa  11074  resqrexlemex  11075  clim0  11334  mertenslem2  11585  infssuzex  11991  bezoutlemmain  12040  ennnfoneleminc  12473  ennnfonelemex  12476  ennnfonelemhom  12477  ennnfonelemr  12485  ctinfom  12490  isnsg2  13167  isbasis2g  14030  tgval2  14036  ntreq0  14117  lmres  14233  eltx  14244  suplociccreex  14587  lgseisenlem2  14937  decidi  15033  nninfsellemqall  15251  nninfomni  15255  trirec0xor  15281