Theorem brralrspcev 5162

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562   ∈ wcel 2144  ∀wral 3078  ∃wrex 3088   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5103

This theorem is referenced by:  axpre-sup  11129  fimaxre2  12139  supaddc  12161  supadd  12162  supmul1  12163  supmullem2  12165  supmul  12166  rpnnen1lem2  12980  iccsupr  13448  supicc  13507  supiccub  13508  supicclub  13509  flval3  13827  fsequb  13990  01sqrexlem3  15273  caubnd2  15387  caubnd  15388  lo1bdd2  15553  lo1bddrp  15554  climcnds  15883  ruclem12  16275  maxprmfct  16746  prmreclem1  16954  prmreclem6  16959  ramz  17063  pgpssslw  19656  gexex  19895  icccmplem2  24886  icccmplem3  24887  reconnlem2  24890  cnllycmp  25020  cncmet  25386  ivthlem2  25516  ivthlem3  25517  cniccbdd  25525  ovolunlem1  25561  ovoliunlem1  25566  ovoliun2  25570  ioombl1lem4  25625  uniioombllem2  25647  uniioombllem6  25652  mbfinf  25729  mbflimsup  25730  itg1climres  25778  itg2i1fseq  25819  itg2i1fseq2  25820  itg2cnlem1  25825  plyeq0lem  26272  ulmbdd  26463  mtestbdd  26470  iblulm  26472  emcllem6  27067  lgambdd  27103  ftalem3  27141  ubthlem2  31076  ubthlem3  31077  htthlem  31122  rge0scvg  34248  esumpcvgval  34377  oddpwdc  34653  mblfinlem3  38163  ismblfin  38165  itg2addnc  38178  ubelsupr  45605  rexabslelem  45997  limsupubuz  46292  liminfreuzlem  46381  dvdivbd  46502  sge0supre  46968  sge0rnbnd  46972  meaiuninc2  47061  hoidmvlelem1  47174  hoidmvlelem4  47177  smfinflem  47396