Theorem brralrspcev 5164

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103

This theorem is used by:  axpre-sup  11255  fimaxre2  12263  supaddc  12285  supadd  12286  supmul1  12287  supmullem2  12289  supmul  12290  rpnnen1lem2  13106  iccsupr  13574  supicc  13633  supiccub  13634  supicclub  13635  flval3  13956  fsequb  14119  01sqrexlem3  15412  caubnd2  15526  caubnd  15527  lo1bdd2  15692  lo1bddrp  15693  climcnds  16021  ruclem12  16410  maxprmfct  16886  prmreclem1  17095  prmreclem6  17100  ramz  17204  pgpssslw  19829  gexex  20068  icccmplem2  25144  icccmplem3  25145  reconnlem2  25148  cnllycmp  25278  cncmet  25644  ivthlem2  25774  ivthlem3  25775  cniccbdd  25783  ovolunlem1  25819  ovoliunlem1  25824  ovoliun2  25828  ioombl1lem4  25883  uniioombllem2  25905  uniioombllem6  25910  mbfinf  25987  mbflimsup  25988  itg1climres  26036  itg2i1fseq  26077  itg2i1fseq2  26078  itg2cnlem1  26083  plyeq0lem  26530  ulmbdd  26726  mtestbdd  26733  iblulm  26735  emcllem6  27329  lgambdd  27365  ftalem3  27403  ubthlem2  31474  ubthlem3  31475  htthlem  31520  rge0scvg  34624  esumpcvgval  34753  oddpwdc  35029  mblfinlem3  38653  ismblfin  38655  itg2addnc  38668  ubelsupr  46113  rexabslelem  46504  limsupubuz  46799  liminfreuzlem  46888  dvdivbd  47009  sge0supre  47475  sge0rnbnd  47479  meaiuninc2  47568  hoidmvlelem1  47681  hoidmvlelem4  47684  smfinflem  47903