Theorem brralrspcev 5208

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  axpre-sup  11207  fimaxre2  12211  supaddc  12233  supadd  12234  supmul1  12235  supmullem2  12237  supmul  12238  rpnnen1lem2  13017  iccsupr  13479  supicc  13538  supiccub  13539  supicclub  13540  flval3  13852  fsequb  14013  01sqrexlem3  15280  caubnd2  15393  caubnd  15394  lo1bdd2  15557  lo1bddrp  15558  climcnds  15884  ruclem12  16274  maxprmfct  16743  prmreclem1  16950  prmreclem6  16955  ramz  17059  pgpssslw  19647  gexex  19886  icccmplem2  24859  icccmplem3  24860  reconnlem2  24863  cnllycmp  25002  cncmet  25370  ivthlem2  25501  ivthlem3  25502  cniccbdd  25510  ovolunlem1  25546  ovoliunlem1  25551  ovoliun2  25555  ioombl1lem4  25610  uniioombllem2  25632  uniioombllem6  25637  mbfinf  25714  mbflimsup  25715  itg1climres  25764  itg2i1fseq  25805  itg2i1fseq2  25806  itg2cnlem1  25811  plyeq0lem  26264  ulmbdd  26456  mtestbdd  26463  iblulm  26465  emcllem6  27059  lgambdd  27095  ftalem3  27133  ubthlem2  30900  ubthlem3  30901  htthlem  30946  rge0scvg  33910  esumpcvgval  34059  oddpwdc  34336  mblfinlem3  37646  ismblfin  37648  itg2addnc  37661  ubelsupr  44958  rexabslelem  45368  limsupubuz  45669  liminfreuzlem  45758  dvdivbd  45879  sge0supre  46345  sge0rnbnd  46349  meaiuninc2  46438  hoidmvlelem1  46551  hoidmvlelem4  46554  smfinflem  46773