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

Theorem brralrspcev 4903
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 4847 . . 3 (𝑥 = 𝐵 → (𝐴𝑅𝑥𝐴𝑅𝐵))
21ralbidv 3167 . 2 (𝑥 = 𝐵 → (∀𝑦𝑌 𝐴𝑅𝑥 ↔ ∀𝑦𝑌 𝐴𝑅𝐵))
32rspcev 3497 1 ((𝐵𝑋 ∧ ∀𝑦𝑌 𝐴𝑅𝐵) → ∃𝑥𝑋𝑦𝑌 𝐴𝑅𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385   = wceq 1653  wcel 2157  wral 3089  wrex 3090   class class class wbr 4843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4844
This theorem is referenced by:  axpre-sup  10278  fimaxre2  11261  supaddc  11282  supadd  11283  supmul1  11284  supmullem2  11286  supmul  11287  rpnnen1lem2  12061  iccsupr  12516  supicc  12574  supiccub  12575  supicclub  12576  flval3  12871  fsequb  13029  sqrlem3  14326  caubnd2  14438  caubnd  14439  lo1bdd2  14596  lo1bddrp  14597  climcnds  14921  ruclem12  15306  maxprmfct  15754  prmreclem1  15953  prmreclem6  15958  ramz  16062  pgpssslw  18342  gexex  18571  icccmplem2  22954  icccmplem3  22955  reconnlem2  22958  cnllycmp  23083  cncmet  23448  ivthlem2  23560  ivthlem3  23561  cniccbdd  23569  ovolunlem1  23605  ovoliunlem1  23610  ovoliun2  23614  ioombl1lem4  23669  uniioombllem2  23691  uniioombllem6  23696  mbfinf  23773  mbflimsup  23774  itg1climres  23822  itg2i1fseq  23863  itg2i1fseq2  23864  itg2cnlem1  23869  plyeq0lem  24307  ulmbdd  24493  mtestbdd  24500  iblulm  24502  emcllem6  25079  lgambdd  25115  ftalem3  25153  ubthlem2  28252  ubthlem3  28253  htthlem  28299  rge0scvg  30511  esumpcvgval  30656  oddpwdc  30932  mblfinlem3  33937  ismblfin  33939  itg2addnc  33952  ubelsupr  39939  rexabslelem  40388  limsupubuz  40689  liminfreuzlem  40778  dvdivbd  40882  sge0supre  41349  sge0rnbnd  41353  meaiuninc2  41442  hoidmvlelem1  41555  hoidmvlelem4  41558  smfinflem  41769
  Copyright terms: Public domain W3C validator