Theorem brralrspcev 5170

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3060  ∃wrex 3069   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111

This theorem is referenced by:  axpre-sup  11114  fimaxre2  12109  supaddc  12131  supadd  12132  supmul1  12133  supmullem2  12135  supmul  12136  rpnnen1lem2  12911  iccsupr  13369  supicc  13428  supiccub  13429  supicclub  13430  flval3  13730  fsequb  13890  01sqrexlem3  15141  caubnd2  15254  caubnd  15255  lo1bdd2  15418  lo1bddrp  15419  climcnds  15747  ruclem12  16134  maxprmfct  16596  prmreclem1  16799  prmreclem6  16804  ramz  16908  pgpssslw  19410  gexex  19645  icccmplem2  24223  icccmplem3  24224  reconnlem2  24227  cnllycmp  24356  cncmet  24723  ivthlem2  24853  ivthlem3  24854  cniccbdd  24862  ovolunlem1  24898  ovoliunlem1  24903  ovoliun2  24907  ioombl1lem4  24962  uniioombllem2  24984  uniioombllem6  24989  mbfinf  25066  mbflimsup  25067  itg1climres  25116  itg2i1fseq  25157  itg2i1fseq2  25158  itg2cnlem1  25163  plyeq0lem  25608  ulmbdd  25794  mtestbdd  25801  iblulm  25803  emcllem6  26387  lgambdd  26423  ftalem3  26461  ubthlem2  29876  ubthlem3  29877  htthlem  29922  rge0scvg  32619  esumpcvgval  32766  oddpwdc  33043  mblfinlem3  36190  ismblfin  36192  itg2addnc  36205  ubelsupr  43347  rexabslelem  43773  limsupubuz  44074  liminfreuzlem  44163  dvdivbd  44284  sge0supre  44750  sge0rnbnd  44754  meaiuninc2  44843  hoidmvlelem1  44956  hoidmvlelem4  44959  smfinflem  45178