Theorem brralrspcev 5135

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ∀wral 3055  ∃wrex 3065   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076

This theorem is referenced by:  axpre-sup  11087  fimaxre2  12096  supaddc  12118  supadd  12119  supmul1  12120  supmullem2  12122  supmul  12123  rpnnen1lem2  12922  iccsupr  13390  supicc  13449  supiccub  13450  supicclub  13451  flval3  13769  fsequb  13932  01sqrexlem3  15201  caubnd2  15315  caubnd  15316  lo1bdd2  15481  lo1bddrp  15482  climcnds  15811  ruclem12  16203  maxprmfct  16674  prmreclem1  16882  prmreclem6  16887  ramz  16991  pgpssslw  19584  gexex  19823  icccmplem2  24811  icccmplem3  24812  reconnlem2  24815  cnllycmp  24945  cncmet  25311  ivthlem2  25441  ivthlem3  25442  cniccbdd  25450  ovolunlem1  25486  ovoliunlem1  25491  ovoliun2  25495  ioombl1lem4  25550  uniioombllem2  25572  uniioombllem6  25577  mbfinf  25654  mbflimsup  25655  itg1climres  25703  itg2i1fseq  25744  itg2i1fseq2  25745  itg2cnlem1  25750  plyeq0lem  26197  ulmbdd  26385  mtestbdd  26392  iblulm  26394  emcllem6  26986  lgambdd  27022  ftalem3  27060  ubthlem2  30964  ubthlem3  30965  htthlem  31010  rge0scvg  34145  esumpcvgval  34274  oddpwdc  34550  mblfinlem3  38041  ismblfin  38043  itg2addnc  38056  ubelsupr  45483  rexabslelem  45875  limsupubuz  46170  liminfreuzlem  46259  dvdivbd  46380  sge0supre  46846  sge0rnbnd  46850  meaiuninc2  46939  hoidmvlelem1  47052  hoidmvlelem4  47055  smfinflem  47274