Theorem brralrspcev 5160

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

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

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  axpre-sup  11094  fimaxre2  12101  supaddc  12123  supadd  12124  supmul1  12125  supmullem2  12127  supmul  12128  rpnnen1lem2  12904  iccsupr  13372  supicc  13431  supiccub  13432  supicclub  13433  flval3  13749  fsequb  13912  01sqrexlem3  15181  caubnd2  15295  caubnd  15296  lo1bdd2  15461  lo1bddrp  15462  climcnds  15788  ruclem12  16180  maxprmfct  16650  prmreclem1  16858  prmreclem6  16863  ramz  16967  pgpssslw  19560  gexex  19799  icccmplem2  24785  icccmplem3  24786  reconnlem2  24789  cnllycmp  24928  cncmet  25295  ivthlem2  25426  ivthlem3  25427  cniccbdd  25435  ovolunlem1  25471  ovoliunlem1  25476  ovoliun2  25480  ioombl1lem4  25535  uniioombllem2  25557  uniioombllem6  25562  mbfinf  25639  mbflimsup  25640  itg1climres  25688  itg2i1fseq  25729  itg2i1fseq2  25730  itg2cnlem1  25735  plyeq0lem  26188  ulmbdd  26380  mtestbdd  26387  iblulm  26389  emcllem6  26984  lgambdd  27020  ftalem3  27058  ubthlem2  30965  ubthlem3  30966  htthlem  31011  rge0scvg  34133  esumpcvgval  34262  oddpwdc  34538  mblfinlem3  37939  ismblfin  37941  itg2addnc  37954  ubelsupr  45409  rexabslelem  45805  limsupubuz  46100  liminfreuzlem  46189  dvdivbd  46310  sge0supre  46776  sge0rnbnd  46780  meaiuninc2  46869  hoidmvlelem1  46982  hoidmvlelem4  46985  smfinflem  47204