Theorem brralrspcev 5226

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  axpre-sup  11238  fimaxre2  12240  supaddc  12262  supadd  12263  supmul1  12264  supmullem2  12266  supmul  12267  rpnnen1lem2  13042  iccsupr  13502  supicc  13561  supiccub  13562  supicclub  13563  flval3  13866  fsequb  14026  01sqrexlem3  15293  caubnd2  15406  caubnd  15407  lo1bdd2  15570  lo1bddrp  15571  climcnds  15899  ruclem12  16289  maxprmfct  16756  prmreclem1  16963  prmreclem6  16968  ramz  17072  pgpssslw  19656  gexex  19895  icccmplem2  24864  icccmplem3  24865  reconnlem2  24868  cnllycmp  25007  cncmet  25375  ivthlem2  25506  ivthlem3  25507  cniccbdd  25515  ovolunlem1  25551  ovoliunlem1  25556  ovoliun2  25560  ioombl1lem4  25615  uniioombllem2  25637  uniioombllem6  25642  mbfinf  25719  mbflimsup  25720  itg1climres  25769  itg2i1fseq  25810  itg2i1fseq2  25811  itg2cnlem1  25816  plyeq0lem  26269  ulmbdd  26459  mtestbdd  26466  iblulm  26468  emcllem6  27062  lgambdd  27098  ftalem3  27136  ubthlem2  30903  ubthlem3  30904  htthlem  30949  rge0scvg  33895  esumpcvgval  34042  oddpwdc  34319  mblfinlem3  37619  ismblfin  37621  itg2addnc  37634  ubelsupr  44920  rexabslelem  45333  limsupubuz  45634  liminfreuzlem  45723  dvdivbd  45844  sge0supre  46310  sge0rnbnd  46314  meaiuninc2  46403  hoidmvlelem1  46516  hoidmvlelem4  46519  smfinflem  46738