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 5061 | . . 3 ⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵)) | |
2 | 1 | ralbidv 3195 | . 2 ⊢ (𝑥 = 𝐵 → (∀𝑦 ∈ 𝑌 𝐴𝑅𝑥 ↔ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵)) |
3 | 2 | rspcev 3621 | 1 ⊢ ((𝐵 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝑌 𝐴𝑅𝐵) → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐴𝑅𝑥) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1531 ∈ wcel 2108 ∀wral 3136 ∃wrex 3137 class class class wbr 5057 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ral 3141 df-rex 3142 df-rab 3145 df-v 3495 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-nul 4290 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-br 5058 |
This theorem is referenced by: axpre-sup 10583 fimaxre2 11578 supaddc 11600 supadd 11601 supmul1 11602 supmullem2 11604 supmul 11605 rpnnen1lem2 12368 iccsupr 12822 supicc 12878 supiccub 12879 supicclub 12880 flval3 13177 fsequb 13335 sqrlem3 14596 caubnd2 14709 caubnd 14710 lo1bdd2 14873 lo1bddrp 14874 climcnds 15198 ruclem12 15586 maxprmfct 16045 prmreclem1 16244 prmreclem6 16249 ramz 16353 pgpssslw 18731 gexex 18965 icccmplem2 23423 icccmplem3 23424 reconnlem2 23427 cnllycmp 23552 cncmet 23917 ivthlem2 24045 ivthlem3 24046 cniccbdd 24054 ovolunlem1 24090 ovoliunlem1 24095 ovoliun2 24099 ioombl1lem4 24154 uniioombllem2 24176 uniioombllem6 24181 mbfinf 24258 mbflimsup 24259 itg1climres 24307 itg2i1fseq 24348 itg2i1fseq2 24349 itg2cnlem1 24354 plyeq0lem 24792 ulmbdd 24978 mtestbdd 24985 iblulm 24987 emcllem6 25570 lgambdd 25606 ftalem3 25644 ubthlem2 28640 ubthlem3 28641 htthlem 28686 rge0scvg 31185 esumpcvgval 31330 oddpwdc 31605 mblfinlem3 34923 ismblfin 34925 itg2addnc 34938 ubelsupr 41268 rexabslelem 41682 limsupubuz 41984 liminfreuzlem 42073 dvdivbd 42198 sge0supre 42662 sge0rnbnd 42666 meaiuninc2 42755 hoidmvlelem1 42868 hoidmvlelem4 42871 smfinflem 43082 |
Copyright terms: Public domain | W3C validator |