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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  axpre-sup  11098  fimaxre2  12104  supaddc  12126  supadd  12127  supmul1  12128  supmullem2  12130  supmul  12131  rpnnen1lem2  12912  iccsupr  13379  supicc  13438  supiccub  13439  supicclub  13440  flval3  13753  fsequb  13916  01sqrexlem3  15186  caubnd2  15300  caubnd  15301  lo1bdd2  15466  lo1bddrp  15467  climcnds  15793  ruclem12  16185  maxprmfct  16655  prmreclem1  16863  prmreclem6  16868  ramz  16972  pgpssslw  19528  gexex  19767  icccmplem2  24745  icccmplem3  24746  reconnlem2  24749  cnllycmp  24888  cncmet  25255  ivthlem2  25386  ivthlem3  25387  cniccbdd  25395  ovolunlem1  25431  ovoliunlem1  25436  ovoliun2  25440  ioombl1lem4  25495  uniioombllem2  25517  uniioombllem6  25522  mbfinf  25599  mbflimsup  25600  itg1climres  25648  itg2i1fseq  25689  itg2i1fseq2  25690  itg2cnlem1  25695  plyeq0lem  26148  ulmbdd  26340  mtestbdd  26347  iblulm  26349  emcllem6  26944  lgambdd  26980  ftalem3  27018  ubthlem2  30850  ubthlem3  30851  htthlem  30896  rge0scvg  33932  esumpcvgval  34061  oddpwdc  34338  mblfinlem3  37646  ismblfin  37648  itg2addnc  37661  ubelsupr  45007  rexabslelem  45407  limsupubuz  45704  liminfreuzlem  45793  dvdivbd  45914  sge0supre  46380  sge0rnbnd  46384  meaiuninc2  46473  hoidmvlelem1  46586  hoidmvlelem4  46589  smfinflem  46808