Theorem brralrspcev 5209

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  axpre-sup  11164  fimaxre2  12159  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  supmul  12186  rpnnen1lem2  12961  iccsupr  13419  supicc  13478  supiccub  13479  supicclub  13480  flval3  13780  fsequb  13940  01sqrexlem3  15191  caubnd2  15304  caubnd  15305  lo1bdd2  15468  lo1bddrp  15469  climcnds  15797  ruclem12  16184  maxprmfct  16646  prmreclem1  16849  prmreclem6  16854  ramz  16958  pgpssslw  19482  gexex  19721  icccmplem2  24339  icccmplem3  24340  reconnlem2  24343  cnllycmp  24472  cncmet  24839  ivthlem2  24969  ivthlem3  24970  cniccbdd  24978  ovolunlem1  25014  ovoliunlem1  25019  ovoliun2  25023  ioombl1lem4  25078  uniioombllem2  25100  uniioombllem6  25105  mbfinf  25182  mbflimsup  25183  itg1climres  25232  itg2i1fseq  25273  itg2i1fseq2  25274  itg2cnlem1  25279  plyeq0lem  25724  ulmbdd  25910  mtestbdd  25917  iblulm  25919  emcllem6  26505  lgambdd  26541  ftalem3  26579  ubthlem2  30124  ubthlem3  30125  htthlem  30170  rge0scvg  32929  esumpcvgval  33076  oddpwdc  33353  mblfinlem3  36527  ismblfin  36529  itg2addnc  36542  ubelsupr  43704  rexabslelem  44128  limsupubuz  44429  liminfreuzlem  44518  dvdivbd  44639  sge0supre  45105  sge0rnbnd  45109  meaiuninc2  45198  hoidmvlelem1  45311  hoidmvlelem4  45314  smfinflem  45533