ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexbii Structured version   Unicode 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

Proof of Theorem rexbii
StepHypRef Expression
1 ralbii.1 . . . 4
21a1i 9 . . 3
32rexbidv 2321 . 2
43trud 1251 1
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  3654  iuncom4  3655  iuniin  3658  dfiunv2  3684  iunab  3694  iunin2  3711  iundif2ss  3713  iunun  3725  iunxiun  3727  iunpwss  3734  inuni  3900  iunopab  4009  sucel  4113  iunpw  4177  xpiundi  4341  xpiundir  4342  reliin  4402  rexxpf  4426  iunxpf  4427  cnvuni  4464  dmiun  4487  dfima3  4614  rniun  4677  dminxp  4708  imaco  4769  coiun  4773  isarep1  4928  rexrn  5247  ralrn  5248  elrnrexdmb  5250  fnasrn  5284  fnasrng  5286  rexima  5337  ralima  5338  abrexco  5341  imaiun  5342  fliftcnv  5378  abrexex2g  5689  abrexex2  5693  qsid  6107  eroveu  6133  genpdflem  6489  genpassl  6506  genpassu  6507  nqprm  6524  nqprrnd  6525  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemopu  6576  elreal  6707  ublbneg  8304  4fvwrd4  8747
  Copyright terms: Public domain W3C validator