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

Theorem rexbii 2309
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 2305 . 2 ( ⊤ → (x A φx A ψ))
43trud 1237 1 (x A φx A ψ)
Colors of variables: wff set class
Syntax hints:  wb 98  wtru 1229  wrex 2285
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-rex 2290
This theorem is referenced by:  2rexbii  2311  r19.29r  2429  r19.42v  2445  rexcom13  2453  rexrot4  2454  3reeanv  2458  cbvrex2v  2520  rexcom4  2554  rexcom4a  2555  rexcom4b  2556  ceqsrex2v  2653  reu7  2713  0el  3218  iuncom  3637  iuncom4  3638  iuniin  3641  dfiunv2  3667  iunab  3677  iunin2  3694  iundif2ss  3696  iunun  3708  iunxiun  3710  iunpwss  3717  inuni  3883  iunopab  3992  sucel  4096  iunpw  4161  xpiundi  4325  xpiundir  4326  reliin  4386  rexxpf  4410  iunxpf  4411  cnvuni  4448  dmiun  4471  dfima3  4598  rniun  4661  dminxp  4692  imaco  4753  coiun  4757  isarep1  4911  rexrn  5229  ralrn  5230  elrnrexdmb  5232  fnasrn  5266  fnasrng  5268  rexima  5319  ralima  5320  abrexco  5323  imaiun  5324  fliftcnv  5360  abrexex2g  5670  abrexex2  5674  qsid  6082  eroveu  6108  genpdflem  6361  genpassl  6379  genpassu  6380  nqprm  6397  nqprrnd  6398  ltexprlemm  6437  ltexprlemopl  6438  ltexprlemopu  6440  elreal  6541
  Copyright terms: Public domain W3C validator