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

Theorem 2rexbidv 2502
Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
2rexbidv (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2rexbidv
StepHypRef Expression
1 2ralbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21rexbidv 2478 . 2 (𝜑 → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
32rexbidv 2478 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wrex 2456
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-rex 2461
This theorem is referenced by:  f1oiso  5829  elrnmpog  5989  elrnmpo  5990  ralrnmpo  5991  rexrnmpo  5992  ovelrn  6025  eroveu  6628  genipv  7510  genpelxp  7512  genpelvl  7513  genpelvu  7514  axcnre  7882  apreap  8546  apreim  8562  aprcl  8605  aptap  8609  bezoutlemnewy  11999  bezoutlema  12002  bezoutlemb  12003  pythagtriplem19  12284  pceu  12297  pcval  12298  pczpre  12299  pcdiv  12304  4sqlem2  12389  4sqlem3  12390  4sqlem4  12392  txuni2  13841  txbas  13843  txdis1cn  13863  2sqlem2  14547  2sqlem8  14555  2sqlem9  14556
  Copyright terms: Public domain W3C validator