Theorem brralrspcev 5159

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3061   class class class wbr 5099

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100

This theorem is referenced by:  axpre-sup  11084  fimaxre2  12091  supaddc  12113  supadd  12114  supmul1  12115  supmullem2  12117  supmul  12118  rpnnen1lem2  12894  iccsupr  13362  supicc  13421  supiccub  13422  supicclub  13423  flval3  13739  fsequb  13902  01sqrexlem3  15171  caubnd2  15285  caubnd  15286  lo1bdd2  15451  lo1bddrp  15452  climcnds  15778  ruclem12  16170  maxprmfct  16640  prmreclem1  16848  prmreclem6  16853  ramz  16957  pgpssslw  19547  gexex  19786  icccmplem2  24772  icccmplem3  24773  reconnlem2  24776  cnllycmp  24915  cncmet  25282  ivthlem2  25413  ivthlem3  25414  cniccbdd  25422  ovolunlem1  25458  ovoliunlem1  25463  ovoliun2  25467  ioombl1lem4  25522  uniioombllem2  25544  uniioombllem6  25549  mbfinf  25626  mbflimsup  25627  itg1climres  25675  itg2i1fseq  25716  itg2i1fseq2  25717  itg2cnlem1  25722  plyeq0lem  26175  ulmbdd  26367  mtestbdd  26374  iblulm  26376  emcllem6  26971  lgambdd  27007  ftalem3  27045  ubthlem2  30950  ubthlem3  30951  htthlem  30996  rge0scvg  34108  esumpcvgval  34237  oddpwdc  34513  mblfinlem3  37862  ismblfin  37864  itg2addnc  37877  ubelsupr  45332  rexabslelem  45729  limsupubuz  46024  liminfreuzlem  46113  dvdivbd  46234  sge0supre  46700  sge0rnbnd  46704  meaiuninc2  46793  hoidmvlelem1  46906  hoidmvlelem4  46909  smfinflem  47128