Theorem brralrspcev 5168

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  axpre-sup  11278  fimaxre2  12286  supaddc  12308  supadd  12309  supmul1  12310  supmullem2  12312  supmul  12313  rpnnen1lem2  13129  iccsupr  13597  supicc  13656  supiccub  13657  supicclub  13658  flval3  13979  fsequb  14142  01sqrexlem3  15437  caubnd2  15551  caubnd  15552  lo1bdd2  15717  lo1bddrp  15718  climcnds  16046  ruclem12  16435  maxprmfct  16911  prmreclem1  17120  prmreclem6  17125  ramz  17229  pgpssslw  19855  gexex  20094  icccmplem2  25170  icccmplem3  25171  reconnlem2  25174  cnllycmp  25304  cncmet  25670  ivthlem2  25800  ivthlem3  25801  cniccbdd  25809  ovolunlem1  25845  ovoliunlem1  25850  ovoliun2  25854  ioombl1lem4  25909  uniioombllem2  25931  uniioombllem6  25936  mbfinf  26013  mbflimsup  26014  itg1climres  26062  itg2i1fseq  26103  itg2i1fseq2  26104  itg2cnlem1  26109  plyeq0lem  26556  ulmbdd  26752  mtestbdd  26759  iblulm  26761  emcllem6  27355  lgambdd  27391  ftalem3  27429  ubthlem2  31500  ubthlem3  31501  htthlem  31546  rge0scvg  34648  esumpcvgval  34777  oddpwdc  35053  mblfinlem3  38768  ismblfin  38770  itg2addnc  38783  ubelsupr  46240  rexabslelem  46631  limsupubuz  46926  liminfreuzlem  47015  dvdivbd  47136  sge0supre  47602  sge0rnbnd  47606  meaiuninc2  47695  hoidmvlelem1  47808  hoidmvlelem4  47811  smfinflem  48030