Theorem brralrspcev 5202

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3060  ∃wrex 3069   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143

This theorem is referenced by:  axpre-sup  11210  fimaxre2  12214  supaddc  12236  supadd  12237  supmul1  12238  supmullem2  12240  supmul  12241  rpnnen1lem2  13020  iccsupr  13483  supicc  13542  supiccub  13543  supicclub  13544  flval3  13856  fsequb  14017  01sqrexlem3  15284  caubnd2  15397  caubnd  15398  lo1bdd2  15561  lo1bddrp  15562  climcnds  15888  ruclem12  16278  maxprmfct  16747  prmreclem1  16955  prmreclem6  16960  ramz  17064  pgpssslw  19633  gexex  19872  icccmplem2  24846  icccmplem3  24847  reconnlem2  24850  cnllycmp  24989  cncmet  25357  ivthlem2  25488  ivthlem3  25489  cniccbdd  25497  ovolunlem1  25533  ovoliunlem1  25538  ovoliun2  25542  ioombl1lem4  25597  uniioombllem2  25619  uniioombllem6  25624  mbfinf  25701  mbflimsup  25702  itg1climres  25750  itg2i1fseq  25791  itg2i1fseq2  25792  itg2cnlem1  25797  plyeq0lem  26250  ulmbdd  26442  mtestbdd  26449  iblulm  26451  emcllem6  27045  lgambdd  27081  ftalem3  27119  ubthlem2  30891  ubthlem3  30892  htthlem  30937  rge0scvg  33949  esumpcvgval  34080  oddpwdc  34357  mblfinlem3  37667  ismblfin  37669  itg2addnc  37682  ubelsupr  45030  rexabslelem  45434  limsupubuz  45733  liminfreuzlem  45822  dvdivbd  45943  sge0supre  46409  sge0rnbnd  46413  meaiuninc2  46502  hoidmvlelem1  46615  hoidmvlelem4  46618  smfinflem  46837