MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brralrspcev Structured version   Visualization version   GIF version

Theorem brralrspcev 5117
Description: Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.)
Assertion
Ref Expression
brralrspcev ((𝐵𝑋 ∧ ∀𝑦𝑌 𝐴𝑅𝐵) → ∃𝑥𝑋𝑦𝑌 𝐴𝑅𝑥)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵,𝑦   𝑥,𝑅   𝑥,𝑋   𝑥,𝑌
Allowed substitution hints:   𝐴(𝑦)   𝑅(𝑦)   𝑋(𝑦)   𝑌(𝑦)

Proof of Theorem brralrspcev
StepHypRef Expression
1 breq2 5061 . . 3 (𝑥 = 𝐵 → (𝐴𝑅𝑥𝐴𝑅𝐵))
21ralbidv 3195 . 2 (𝑥 = 𝐵 → (∀𝑦𝑌 𝐴𝑅𝑥 ↔ ∀𝑦𝑌 𝐴𝑅𝐵))
32rspcev 3621 1 ((𝐵𝑋 ∧ ∀𝑦𝑌 𝐴𝑅𝐵) → ∃𝑥𝑋𝑦𝑌 𝐴𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1530  wcel 2107  wral 3136  wrex 3137   class class class wbr 5057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058
This theorem is referenced by:  axpre-sup  10583  fimaxre2  11578  supaddc  11600  supadd  11601  supmul1  11602  supmullem2  11604  supmul  11605  rpnnen1lem2  12368  iccsupr  12822  supicc  12878  supiccub  12879  supicclub  12880  flval3  13177  fsequb  13335  sqrlem3  14596  caubnd2  14709  caubnd  14710  lo1bdd2  14873  lo1bddrp  14874  climcnds  15198  ruclem12  15586  maxprmfct  16045  prmreclem1  16244  prmreclem6  16249  ramz  16353  pgpssslw  18731  gexex  18965  icccmplem2  23423  icccmplem3  23424  reconnlem2  23427  cnllycmp  23552  cncmet  23917  ivthlem2  24045  ivthlem3  24046  cniccbdd  24054  ovolunlem1  24090  ovoliunlem1  24095  ovoliun2  24099  ioombl1lem4  24154  uniioombllem2  24176  uniioombllem6  24181  mbfinf  24258  mbflimsup  24259  itg1climres  24307  itg2i1fseq  24348  itg2i1fseq2  24349  itg2cnlem1  24354  plyeq0lem  24792  ulmbdd  24978  mtestbdd  24985  iblulm  24987  emcllem6  25570  lgambdd  25606  ftalem3  25644  ubthlem2  28640  ubthlem3  28641  htthlem  28686  rge0scvg  31180  esumpcvgval  31325  oddpwdc  31600  mblfinlem3  34918  ismblfin  34920  itg2addnc  34933  ubelsupr  41262  rexabslelem  41676  limsupubuz  41978  liminfreuzlem  42067  dvdivbd  42192  sge0supre  42656  sge0rnbnd  42660  meaiuninc2  42749  hoidmvlelem1  42862  hoidmvlelem4  42865  smfinflem  43076
  Copyright terms: Public domain W3C validator