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  5820  elrnmpog  5980  elrnmpo  5981  ralrnmpo  5982  rexrnmpo  5983  ovelrn  6016  eroveu  6619  genipv  7486  genpelxp  7488  genpelvl  7489  genpelvu  7490  axcnre  7858  apreap  8521  apreim  8537  aprcl  8580  bezoutlemnewy  11967  bezoutlema  11970  bezoutlemb  11971  pythagtriplem19  12252  pceu  12265  pcval  12266  pczpre  12267  pcdiv  12272  4sqlem2  12357  4sqlem3  12358  4sqlem4  12360  txuni2  13389  txbas  13391  txdis1cn  13411  2sqlem2  14084  2sqlem8  14092  2sqlem9  14093
  Copyright terms: Public domain W3C validator