ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralbii GIF version

Theorem ralbii 2441
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
StepHypRef Expression
1 ralbii.1 . . . 4 (𝜑𝜓)
21a1i 9 . . 3 (⊤ → (𝜑𝜓))
32ralbidv 2437 . 2 (⊤ → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
43mptru 1340 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wtru 1332  wral 2416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-ral 2421
This theorem is referenced by:  2ralbii  2443  ralinexa  2462  r3al  2477  r19.26-2  2561  r19.26-3  2562  ralbiim  2566  r19.28av  2568  ralnex2  2571  cbvral2v  2665  cbvral3v  2667  sbralie  2670  ralcom4  2708  reu8  2880  2reuswapdc  2888  r19.12sn  3589  eqsnm  3682  uni0b  3761  uni0c  3762  ssint  3787  iuniin  3823  iuneq2  3829  iunss  3854  ssiinf  3862  iinab  3874  iindif2m  3880  iinin2m  3881  iinuniss  3895  sspwuni  3897  iinpw  3903  dftr3  4030  trint  4041  bnd2  4097  reusv3  4381  reg2exmidlema  4449  setindel  4453  ordsoexmid  4477  zfregfr  4488  tfi  4496  tfis2f  4498  ssrel2  4629  reliun  4660  xpiindim  4676  ralxpf  4685  dfse2  4912  rninxp  4982  dminxp  4983  cnviinm  5080  cnvpom  5081  cnvsom  5082  dffun9  5152  funco  5163  funcnv3  5185  fncnv  5189  funimaexglem  5206  fnres  5239  fnopabg  5246  mptfng  5248  fintm  5308  f1ompt  5571  idref  5658  dff13f  5671  foov  5917  tfr1onlemaccex  6245  tfrcllembxssdm  6253  tfrcllemaccex  6258  oacl  6356  ixpeq2  6606  ixpin  6617  ixpiinm  6618  infmoti  6915  acfun  7068  ccfunen  7084  cc2  7087  cc4f  7089  cc4n  7091  cauappcvgprlemladdrl  7477  axcaucvglemres  7719  axpre-suploc  7722  dfinfre  8726  suprzclex  9161  supinfneg  9402  infsupneg  9403  cvg1nlemcau  10768  cvg1nlemres  10769  rexfiuz  10773  recvguniq  10779  resqrexlemglsq  10806  resqrexlemsqa  10808  resqrexlemex  10809  clim0  11066  mertenslem2  11317  infssuzex  11653  bezoutlemmain  11697  ennnfoneleminc  11935  ennnfonelemex  11938  ennnfonelemhom  11939  ennnfonelemr  11947  ctinfom  11952  isbasis2g  12226  tgval2  12234  ntreq0  12315  lmres  12431  eltx  12442  suplociccreex  12785  decidi  13061  nninfsellemqall  13272  nninfomni  13276  trirec0xor  13299
  Copyright terms: Public domain W3C validator