Theorem brralrspcev 5167

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

Step	Hyp	Ref	Expression
1		breq2 5111	. . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵))
2	1	ralbidv 3156	. 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵))
3	2	rspcev 3588	1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  axpre-sup  11122  fimaxre2  12128  supaddc  12150  supadd  12151  supmul1  12152  supmullem2  12154  supmul  12155  rpnnen1lem2  12936  iccsupr  13403  supicc  13462  supiccub  13463  supicclub  13464  flval3  13777  fsequb  13940  01sqrexlem3  15210  caubnd2  15324  caubnd  15325  lo1bdd2  15490  lo1bddrp  15491  climcnds  15817  ruclem12  16209  maxprmfct  16679  prmreclem1  16887  prmreclem6  16892  ramz  16996  pgpssslw  19544  gexex  19783  icccmplem2  24712  icccmplem3  24713  reconnlem2  24716  cnllycmp  24855  cncmet  25222  ivthlem2  25353  ivthlem3  25354  cniccbdd  25362  ovolunlem1  25398  ovoliunlem1  25403  ovoliun2  25407  ioombl1lem4  25462  uniioombllem2  25484  uniioombllem6  25489  mbfinf  25566  mbflimsup  25567  itg1climres  25615  itg2i1fseq  25656  itg2i1fseq2  25657  itg2cnlem1  25662  plyeq0lem  26115  ulmbdd  26307  mtestbdd  26314  iblulm  26316  emcllem6  26911  lgambdd  26947  ftalem3  26985  ubthlem2  30800  ubthlem3  30801  htthlem  30846  rge0scvg  33939  esumpcvgval  34068  oddpwdc  34345  mblfinlem3  37653  ismblfin  37655  itg2addnc  37668  ubelsupr  45014  rexabslelem  45414  limsupubuz  45711  liminfreuzlem  45800  dvdivbd  45921  sge0supre  46387  sge0rnbnd  46391  meaiuninc2  46480  hoidmvlelem1  46593  hoidmvlelem4  46596  smfinflem  46815