Theorem brralrspcev 5162

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 5106	. . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵))
2	1	ralbidv 3156	. 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵))
3	2	rspcev 3585	1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥)

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

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  axpre-sup  11100  fimaxre2  12106  supaddc  12128  supadd  12129  supmul1  12130  supmullem2  12132  supmul  12133  rpnnen1lem2  12914  iccsupr  13381  supicc  13440  supiccub  13441  supicclub  13442  flval3  13755  fsequb  13918  01sqrexlem3  15187  caubnd2  15301  caubnd  15302  lo1bdd2  15467  lo1bddrp  15468  climcnds  15794  ruclem12  16186  maxprmfct  16656  prmreclem1  16864  prmreclem6  16869  ramz  16973  pgpssslw  19529  gexex  19768  icccmplem2  24746  icccmplem3  24747  reconnlem2  24750  cnllycmp  24889  cncmet  25256  ivthlem2  25387  ivthlem3  25388  cniccbdd  25396  ovolunlem1  25432  ovoliunlem1  25437  ovoliun2  25441  ioombl1lem4  25496  uniioombllem2  25518  uniioombllem6  25523  mbfinf  25600  mbflimsup  25601  itg1climres  25649  itg2i1fseq  25690  itg2i1fseq2  25691  itg2cnlem1  25696  plyeq0lem  26149  ulmbdd  26341  mtestbdd  26348  iblulm  26350  emcllem6  26945  lgambdd  26981  ftalem3  27019  ubthlem2  30851  ubthlem3  30852  htthlem  30897  rge0scvg  33933  esumpcvgval  34062  oddpwdc  34339  mblfinlem3  37647  ismblfin  37649  itg2addnc  37662  ubelsupr  45008  rexabslelem  45408  limsupubuz  45705  liminfreuzlem  45794  dvdivbd  45915  sge0supre  46381  sge0rnbnd  46385  meaiuninc2  46474  hoidmvlelem1  46587  hoidmvlelem4  46590  smfinflem  46809