Theorem brralrspcev 5184

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3052  ∃wrex 3061   class class class wbr 5124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  axpre-sup  11188  fimaxre2  12192  supaddc  12214  supadd  12215  supmul1  12216  supmullem2  12218  supmul  12219  rpnnen1lem2  12998  iccsupr  13464  supicc  13523  supiccub  13524  supicclub  13525  flval3  13837  fsequb  13998  01sqrexlem3  15268  caubnd2  15381  caubnd  15382  lo1bdd2  15545  lo1bddrp  15546  climcnds  15872  ruclem12  16264  maxprmfct  16733  prmreclem1  16941  prmreclem6  16946  ramz  17050  pgpssslw  19600  gexex  19839  icccmplem2  24768  icccmplem3  24769  reconnlem2  24772  cnllycmp  24911  cncmet  25279  ivthlem2  25410  ivthlem3  25411  cniccbdd  25419  ovolunlem1  25455  ovoliunlem1  25460  ovoliun2  25464  ioombl1lem4  25519  uniioombllem2  25541  uniioombllem6  25546  mbfinf  25623  mbflimsup  25624  itg1climres  25672  itg2i1fseq  25713  itg2i1fseq2  25714  itg2cnlem1  25719  plyeq0lem  26172  ulmbdd  26364  mtestbdd  26371  iblulm  26373  emcllem6  26968  lgambdd  27004  ftalem3  27042  ubthlem2  30857  ubthlem3  30858  htthlem  30903  rge0scvg  33985  esumpcvgval  34114  oddpwdc  34391  mblfinlem3  37688  ismblfin  37690  itg2addnc  37703  ubelsupr  45011  rexabslelem  45412  limsupubuz  45709  liminfreuzlem  45798  dvdivbd  45919  sge0supre  46385  sge0rnbnd  46389  meaiuninc2  46478  hoidmvlelem1  46591  hoidmvlelem4  46594  smfinflem  46813