|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > brralrspcev | Structured version Visualization version GIF version | ||
| Description: Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) | 
| Ref | Expression | 
|---|---|
| brralrspcev | ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | breq2 5146 | . . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵)) | |
| 2 | 1 | ralbidv 3177 | . 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵)) | 
| 3 | 2 | rspcev 3621 | 1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) | 
| Colors of variables: wff setvar class | 
| 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 | 
| Copyright terms: Public domain | W3C validator |