Theorem brralrspcev 5170

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569   ∈ wcel 2142  ∀wral 3078  ∃wrex 3088   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109

This theorem is used by:  axpre-sup  11160  fimaxre2  12166  supaddc  12188  supadd  12189  supmul1  12190  supmullem2  12192  supmul  12193  rpnnen1lem2  13007  iccsupr  13475  supicc  13534  supiccub  13535  supicclub  13536  flval3  13855  fsequb  14018  01sqrexlem3  15302  caubnd2  15416  caubnd  15417  lo1bdd2  15582  lo1bddrp  15583  climcnds  15912  ruclem12  16303  maxprmfct  16774  prmreclem1  16982  prmreclem6  16987  ramz  17091  pgpssslw  19690  gexex  19929  icccmplem2  24992  icccmplem3  24993  reconnlem2  24996  cnllycmp  25126  cncmet  25492  ivthlem2  25622  ivthlem3  25623  cniccbdd  25631  ovolunlem1  25667  ovoliunlem1  25672  ovoliun2  25676  ioombl1lem4  25731  uniioombllem2  25753  uniioombllem6  25758  mbfinf  25835  mbflimsup  25836  itg1climres  25884  itg2i1fseq  25925  itg2i1fseq2  25926  itg2cnlem1  25931  plyeq0lem  26378  ulmbdd  26572  mtestbdd  26579  iblulm  26581  emcllem6  27176  lgambdd  27212  ftalem3  27250  ubthlem2  31234  ubthlem3  31235  htthlem  31280  rge0scvg  34348  esumpcvgval  34477  oddpwdc  34753  mblfinlem3  38338  ismblfin  38340  itg2addnc  38353  ubelsupr  45768  rexabslelem  46160  limsupubuz  46455  liminfreuzlem  46544  dvdivbd  46665  sge0supre  47131  sge0rnbnd  47135  meaiuninc2  47224  hoidmvlelem1  47337  hoidmvlelem4  47340  smfinflem  47559