Theorem brralrspcev 5169

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088   class class class wbr 5107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  axpre-sup  11181  fimaxre2  12187  supaddc  12209  supadd  12210  supmul1  12211  supmullem2  12213  supmul  12214  rpnnen1lem2  13029  iccsupr  13497  supicc  13556  supiccub  13557  supicclub  13558  flval3  13878  fsequb  14041  01sqrexlem3  15333  caubnd2  15447  caubnd  15448  lo1bdd2  15613  lo1bddrp  15614  climcnds  15942  ruclem12  16333  maxprmfct  16804  prmreclem1  17012  prmreclem6  17017  ramz  17121  pgpssslw  19742  gexex  19981  icccmplem2  25051  icccmplem3  25052  reconnlem2  25055  cnllycmp  25185  cncmet  25551  ivthlem2  25681  ivthlem3  25682  cniccbdd  25690  ovolunlem1  25726  ovoliunlem1  25731  ovoliun2  25735  ioombl1lem4  25790  uniioombllem2  25812  uniioombllem6  25817  mbfinf  25894  mbflimsup  25895  itg1climres  25943  itg2i1fseq  25984  itg2i1fseq2  25985  itg2cnlem1  25990  plyeq0lem  26437  ulmbdd  26631  mtestbdd  26638  iblulm  26640  emcllem6  27235  lgambdd  27271  ftalem3  27309  ubthlem2  31338  ubthlem3  31339  htthlem  31384  rge0scvg  34446  esumpcvgval  34575  oddpwdc  34852  mblfinlem3  38395  ismblfin  38397  itg2addnc  38410  ubelsupr  45841  rexabslelem  46233  limsupubuz  46528  liminfreuzlem  46617  dvdivbd  46738  sge0supre  47204  sge0rnbnd  47208  meaiuninc2  47297  hoidmvlelem1  47410  hoidmvlelem4  47413  smfinflem  47632