![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2rexbidva | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.) |
Ref | Expression |
---|---|
2ralbidva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2rexbidva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) | |
2 | 1 | anassrs 467 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | rexbidva 3175 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | rexbidva 3175 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2106 ∃wrex 3068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-rex 3069 |
This theorem is referenced by: 2reu4lem 4528 wrdl3s3 14998 bezoutlem2 16574 bezoutlem4 16576 vdwmc2 17013 lsmcom2 19688 lsmass 19702 lsmcomx 19889 lsmspsn 21101 hausdiag 23669 imasf1oxms 24518 mulsval 28150 mulscom 28180 addsdi 28196 mulsasslem3 28206 mulsunif2lem 28210 istrkg2ld 28483 iscgra 28832 axeuclid 28993 elwwlks2 29996 elwspths2spth 29997 fusgr2wsp2nb 30363 shscom 31348 lsmssass 33410 sategoelfvb 35404 3dim0 39440 islpln5 39518 islvol5 39562 isline2 39757 isline3 39759 paddcom 39796 cdlemg2cex 40574 prprspr2 47443 pgrpgt2nabl 48211 elbigolo1 48407 |
Copyright terms: Public domain | W3C validator |