Theorem brralrspcev 5134

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3049  ∃wrex 3059   class class class wbr 5074

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075

This theorem is referenced by:  axpre-sup  11081  fimaxre2  12090  supaddc  12112  supadd  12113  supmul1  12114  supmullem2  12116  supmul  12117  rpnnen1lem2  12916  iccsupr  13384  supicc  13443  supiccub  13444  supicclub  13445  flval3  13763  fsequb  13926  01sqrexlem3  15195  caubnd2  15309  caubnd  15310  lo1bdd2  15475  lo1bddrp  15476  climcnds  15805  ruclem12  16197  maxprmfct  16668  prmreclem1  16876  prmreclem6  16881  ramz  16985  pgpssslw  19578  gexex  19817  icccmplem2  24777  icccmplem3  24778  reconnlem2  24781  cnllycmp  24911  cncmet  25277  ivthlem2  25407  ivthlem3  25408  cniccbdd  25416  ovolunlem1  25452  ovoliunlem1  25457  ovoliun2  25461  ioombl1lem4  25516  uniioombllem2  25538  uniioombllem6  25543  mbfinf  25620  mbflimsup  25621  itg1climres  25669  itg2i1fseq  25710  itg2i1fseq2  25711  itg2cnlem1  25716  plyeq0lem  26163  ulmbdd  26351  mtestbdd  26358  iblulm  26360  emcllem6  26952  lgambdd  26988  ftalem3  27026  ubthlem2  30930  ubthlem3  30931  htthlem  30976  rge0scvg  34081  esumpcvgval  34210  oddpwdc  34486  mblfinlem3  37968  ismblfin  37970  itg2addnc  37983  ubelsupr  45439  rexabslelem  45834  limsupubuz  46129  liminfreuzlem  46218  dvdivbd  46339  sge0supre  46805  sge0rnbnd  46809  meaiuninc2  46898  hoidmvlelem1  47011  hoidmvlelem4  47014  smfinflem  47233