Theorem brralrspcev 5149

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  axpre-sup  11060  fimaxre2  12067  supaddc  12089  supadd  12090  supmul1  12091  supmullem2  12093  supmul  12094  rpnnen1lem2  12875  iccsupr  13342  supicc  13401  supiccub  13402  supicclub  13403  flval3  13719  fsequb  13882  01sqrexlem3  15151  caubnd2  15265  caubnd  15266  lo1bdd2  15431  lo1bddrp  15432  climcnds  15758  ruclem12  16150  maxprmfct  16620  prmreclem1  16828  prmreclem6  16833  ramz  16937  pgpssslw  19526  gexex  19765  icccmplem2  24739  icccmplem3  24740  reconnlem2  24743  cnllycmp  24882  cncmet  25249  ivthlem2  25380  ivthlem3  25381  cniccbdd  25389  ovolunlem1  25425  ovoliunlem1  25430  ovoliun2  25434  ioombl1lem4  25489  uniioombllem2  25511  uniioombllem6  25516  mbfinf  25593  mbflimsup  25594  itg1climres  25642  itg2i1fseq  25683  itg2i1fseq2  25684  itg2cnlem1  25689  plyeq0lem  26142  ulmbdd  26334  mtestbdd  26341  iblulm  26343  emcllem6  26938  lgambdd  26974  ftalem3  27012  ubthlem2  30851  ubthlem3  30852  htthlem  30897  rge0scvg  33962  esumpcvgval  34091  oddpwdc  34367  mblfinlem3  37698  ismblfin  37700  itg2addnc  37713  ubelsupr  45116  rexabslelem  45515  limsupubuz  45810  liminfreuzlem  45899  dvdivbd  46020  sge0supre  46486  sge0rnbnd  46490  meaiuninc2  46579  hoidmvlelem1  46692  hoidmvlelem4  46695  smfinflem  46914