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

Theorem rexbii 2325
Description: Inference adding restricted existential 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
rexbii (x A φx A ψ)

Proof of Theorem rexbii
StepHypRef Expression
1 ralbii.1 . . . 4 (φψ)
21a1i 9 . . 3 ( ⊤ → (φψ))
32rexbidv 2321 . 2 ( ⊤ → (x A φx A ψ))
43trud 1251 1 (x A φx A ψ)
Colors of variables: wff set class
Syntax hints:  wb 98  wtru 1243  wrex 2301
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-rex 2306
This theorem is referenced by:  2rexbii  2327  r19.29r  2445  r19.42v  2461  rexcom13  2469  rexrot4  2470  3reeanv  2474  cbvrex2v  2536  rexcom4  2571  rexcom4a  2572  rexcom4b  2573  ceqsrex2v  2670  reu7  2730  0el  3235  iuncom  3653  iuncom4  3654  iuniin  3657  dfiunv2  3683  iunab  3693  iunin2  3710  iundif2ss  3712  iunun  3724  iunxiun  3726  iunpwss  3733  inuni  3899  iunopab  4008  sucel  4112  iunpw  4176  xpiundi  4340  xpiundir  4341  reliin  4401  rexxpf  4425  iunxpf  4426  cnvuni  4463  dmiun  4486  dfima3  4613  rniun  4676  dminxp  4707  imaco  4768  coiun  4772  isarep1  4926  rexrn  5245  ralrn  5246  elrnrexdmb  5248  fnasrn  5282  fnasrng  5284  rexima  5335  ralima  5336  abrexco  5339  imaiun  5340  fliftcnv  5376  abrexex2g  5686  abrexex2  5690  qsid  6100  eroveu  6126  genpdflem  6482  genpassl  6500  genpassu  6501  nqprm  6518  nqprrnd  6519  ltexprlemm  6564  ltexprlemopl  6565  ltexprlemopu  6567  elreal  6679  ublbneg  8273  4fvwrd4  8713
  Copyright terms: Public domain W3C validator