Theorem brralrspcev 5146

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

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

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

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  24803  icccmplem3  24804  reconnlem2  24807  cnllycmp  24937  cncmet  25303  ivthlem2  25433  ivthlem3  25434  cniccbdd  25442  ovolunlem1  25478  ovoliunlem1  25483  ovoliun2  25487  ioombl1lem4  25542  uniioombllem2  25564  uniioombllem6  25569  mbfinf  25646  mbflimsup  25647  itg1climres  25695  itg2i1fseq  25736  itg2i1fseq2  25737  itg2cnlem1  25742  plyeq0lem  26189  ulmbdd  26380  mtestbdd  26387  iblulm  26389  emcllem6  26982  lgambdd  27018  ftalem3  27056  ubthlem2  30961  ubthlem3  30962  htthlem  31007  rge0scvg  34113  esumpcvgval  34242  oddpwdc  34518  mblfinlem3  38000  ismblfin  38002  itg2addnc  38015  ubelsupr  45475  rexabslelem  45870  limsupubuz  46165  liminfreuzlem  46254  dvdivbd  46375  sge0supre  46841  sge0rnbnd  46845  meaiuninc2  46934  hoidmvlelem1  47047  hoidmvlelem4  47050  smfinflem  47269