Theorem brralrspcev 5152

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053   class class class wbr 5092

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093

This theorem is referenced by:  axpre-sup  11063  fimaxre2  12070  supaddc  12092  supadd  12093  supmul1  12094  supmullem2  12096  supmul  12097  rpnnen1lem2  12878  iccsupr  13345  supicc  13404  supiccub  13405  supicclub  13406  flval3  13719  fsequb  13882  01sqrexlem3  15151  caubnd2  15265  caubnd  15266  lo1bdd2  15431  lo1bddrp  15432  climcnds  15758  ruclem12  16150  maxprmfct  16620  prmreclem1  16828  prmreclem6  16833  ramz  16937  pgpssslw  19493  gexex  19732  icccmplem2  24710  icccmplem3  24711  reconnlem2  24714  cnllycmp  24853  cncmet  25220  ivthlem2  25351  ivthlem3  25352  cniccbdd  25360  ovolunlem1  25396  ovoliunlem1  25401  ovoliun2  25405  ioombl1lem4  25460  uniioombllem2  25482  uniioombllem6  25487  mbfinf  25564  mbflimsup  25565  itg1climres  25613  itg2i1fseq  25654  itg2i1fseq2  25655  itg2cnlem1  25660  plyeq0lem  26113  ulmbdd  26305  mtestbdd  26312  iblulm  26314  emcllem6  26909  lgambdd  26945  ftalem3  26983  ubthlem2  30819  ubthlem3  30820  htthlem  30865  rge0scvg  33932  esumpcvgval  34061  oddpwdc  34338  mblfinlem3  37659  ismblfin  37661  itg2addnc  37674  ubelsupr  45018  rexabslelem  45417  limsupubuz  45714  liminfreuzlem  45803  dvdivbd  45924  sge0supre  46390  sge0rnbnd  46394  meaiuninc2  46483  hoidmvlelem1  46596  hoidmvlelem4  46599  smfinflem  46818