Theorem brralrspcev 5141

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539   ∈ wcel 2104  ∀wral 3062  ∃wrex 3071   class class class wbr 5081

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082

This theorem is referenced by:  axpre-sup  10971  fimaxre2  11966  supaddc  11988  supadd  11989  supmul1  11990  supmullem2  11992  supmul  11993  rpnnen1lem2  12763  iccsupr  13220  supicc  13279  supiccub  13280  supicclub  13281  flval3  13581  fsequb  13741  sqrlem3  15001  caubnd2  15114  caubnd  15115  lo1bdd2  15278  lo1bddrp  15279  climcnds  15608  ruclem12  15995  maxprmfct  16459  prmreclem1  16662  prmreclem6  16667  ramz  16771  pgpssslw  19264  gexex  19499  icccmplem2  24031  icccmplem3  24032  reconnlem2  24035  cnllycmp  24164  cncmet  24531  ivthlem2  24661  ivthlem3  24662  cniccbdd  24670  ovolunlem1  24706  ovoliunlem1  24711  ovoliun2  24715  ioombl1lem4  24770  uniioombllem2  24792  uniioombllem6  24797  mbfinf  24874  mbflimsup  24875  itg1climres  24924  itg2i1fseq  24965  itg2i1fseq2  24966  itg2cnlem1  24971  plyeq0lem  25416  ulmbdd  25602  mtestbdd  25609  iblulm  25611  emcllem6  26195  lgambdd  26231  ftalem3  26269  ubthlem2  29278  ubthlem3  29279  htthlem  29324  rge0scvg  31944  esumpcvgval  32091  oddpwdc  32366  mblfinlem3  35860  ismblfin  35862  itg2addnc  35875  ubelsupr  42601  rexabslelem  43006  limsupubuz  43303  liminfreuzlem  43392  dvdivbd  43513  sge0supre  43977  sge0rnbnd  43981  meaiuninc2  44070  hoidmvlelem1  44183  hoidmvlelem4  44186  smfinflem  44404