Theorem brralrspcev 5138

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2109  ∀wral 3065  ∃wrex 3066   class class class wbr 5078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079

This theorem is referenced by:  axpre-sup  10909  fimaxre2  11903  supaddc  11925  supadd  11926  supmul1  11927  supmullem2  11929  supmul  11930  rpnnen1lem2  12699  iccsupr  13156  supicc  13215  supiccub  13216  supicclub  13217  flval3  13516  fsequb  13676  sqrlem3  14937  caubnd2  15050  caubnd  15051  lo1bdd2  15214  lo1bddrp  15215  climcnds  15544  ruclem12  15931  maxprmfct  16395  prmreclem1  16598  prmreclem6  16603  ramz  16707  pgpssslw  19200  gexex  19435  icccmplem2  23967  icccmplem3  23968  reconnlem2  23971  cnllycmp  24100  cncmet  24467  ivthlem2  24597  ivthlem3  24598  cniccbdd  24606  ovolunlem1  24642  ovoliunlem1  24647  ovoliun2  24651  ioombl1lem4  24706  uniioombllem2  24728  uniioombllem6  24733  mbfinf  24810  mbflimsup  24811  itg1climres  24860  itg2i1fseq  24901  itg2i1fseq2  24902  itg2cnlem1  24907  plyeq0lem  25352  ulmbdd  25538  mtestbdd  25545  iblulm  25547  emcllem6  26131  lgambdd  26167  ftalem3  26205  ubthlem2  29212  ubthlem3  29213  htthlem  29258  rge0scvg  31878  esumpcvgval  32025  oddpwdc  32300  mblfinlem3  35795  ismblfin  35797  itg2addnc  35810  ubelsupr  42516  rexabslelem  42912  limsupubuz  43208  liminfreuzlem  43297  dvdivbd  43418  sge0supre  43881  sge0rnbnd  43885  meaiuninc2  43974  hoidmvlelem1  44087  hoidmvlelem4  44090  smfinflem  44301