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  11254  fimaxre2  12262  supaddc  12284  supadd  12285  supmul1  12286  supmullem2  12288  supmul  12289  rpnnen1lem2  13105  iccsupr  13573  supicc  13632  supiccub  13633  supicclub  13634  flval3  13955  fsequb  14118  01sqrexlem3  15411  caubnd2  15525  caubnd  15526  lo1bdd2  15691  lo1bddrp  15692  climcnds  16020  ruclem12  16409  maxprmfct  16885  prmreclem1  17094  prmreclem6  17099  ramz  17203  pgpssslw  19828  gexex  20067  icccmplem2  25143  icccmplem3  25144  reconnlem2  25147  cnllycmp  25277  cncmet  25643  ivthlem2  25773  ivthlem3  25774  cniccbdd  25782  ovolunlem1  25818  ovoliunlem1  25823  ovoliun2  25827  ioombl1lem4  25882  uniioombllem2  25904  uniioombllem6  25909  mbfinf  25986  mbflimsup  25987  itg1climres  26035  itg2i1fseq  26076  itg2i1fseq2  26077  itg2cnlem1  26082  plyeq0lem  26529  ulmbdd  26725  mtestbdd  26732  iblulm  26734  emcllem6  27328  lgambdd  27364  ftalem3  27402  ubthlem2  31473  ubthlem3  31474  htthlem  31519  rge0scvg  34581  esumpcvgval  34710  oddpwdc  34986  mblfinlem3  38578  ismblfin  38580  itg2addnc  38593  ubelsupr  46037  rexabslelem  46428  limsupubuz  46723  liminfreuzlem  46812  dvdivbd  46933  sge0supre  47399  sge0rnbnd  47403  meaiuninc2  47492  hoidmvlelem1  47605  hoidmvlelem4  47608  smfinflem  47827